- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b17f1c8-f0ea-46ad-b399-1a0dffaf3bc5
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 1 <= mid
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b7576d2-4946-479f-9b8e-d499cf52a3ab
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 29
    column: 4
    function: main
  location_invariant:
    string: mid <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 05a44964-e66d-413f-ab5c-238ae9b2f9b2
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 29
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )mid >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c2391c9-38f6-441c-b94f-1e3e237e2360
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 1000000LL - (long long )mid >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e4919350-4381-4bc8-93b3-62f925fd3335
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 29
    column: 4
    function: main
  location_invariant:
    string: mid != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9c436c4b-fca5-4a6e-9895-81e66f7b36ea
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 31
    column: 8
    function: main
  location_invariant:
    string: 0 <= lo
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d2f5c8bb-1ebe-46b7-af2b-43ac02f4564f
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 31
    column: 8
    function: main
  location_invariant:
    string: lo <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e7338aa-a20a-4786-8657-977c523ec42e
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 31
    column: 8
    function: main
  location_invariant:
    string: (-2LL + (long long )hi) - (long long )lo >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b1d6d27b-f257-488b-b764-9fe8d5e1a4b8
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 31
    column: 8
    function: main
  location_invariant:
    string: (2000000LL - (long long )hi) - (long long )lo >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 38e35aff-a5de-4126-b137-a784d1fe2426
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 31
    column: 8
    function: main
  location_invariant:
    string: (long long )lo >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 551e08e6-11ab-42d4-9117-3cd58a4295a6
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 32
    column: 8
    function: main
  location_invariant:
    string: 1 <= lo
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c84cee77-3457-42ff-ad95-c08a94311c35
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 32
    column: 8
    function: main
  location_invariant:
    string: 1 <= hi
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 585fd69b-3f0f-454d-92ad-923ffb9551ae
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 32
    column: 8
    function: main
  location_invariant:
    string: lo <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 60f3627a-59a6-4bd4-b2fe-2d16414a6805
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 32
    column: 8
    function: main
  location_invariant:
    string: hi <= 2000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a521474-0fc9-417b-8141-76c8871d1f36
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 32
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )lo >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 854acd95-26dc-4fc0-8559-41155da4c306
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 32
    column: 8
    function: main
  location_invariant:
    string: (-1LL + (long long )hi) - (long long )lo >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b56922ab-1aae-4148-aba7-2cd187b7ff74
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 32
    column: 8
    function: main
  location_invariant:
    string: (2000001LL - (long long )hi) - (long long )lo >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 699ca868-6bac-4c17-b160-9aaf98b4dbe3
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 33
    column: 8
    function: main
  location_invariant:
    string: 1 <= mid
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 37a8b301-02e1-4320-8b97-a6b9ffd0ff29
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 33
    column: 8
    function: main
  location_invariant:
    string: 1 <= hi
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 108590df-e5ba-460a-b3be-45b7d40fbff9
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 33
    column: 8
    function: main
  location_invariant:
    string: mid <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a2e8a721-f8f2-40b2-a346-7007137506ae
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 33
    column: 8
    function: main
  location_invariant:
    string: hi <= 1999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d549074-5c78-4871-b13e-188de483a003
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 33
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )lo >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9553ea2b-9e79-4294-bfb0-6edf3b5ee5bc
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 33
    column: 8
    function: main
  location_invariant:
    string: (2000000LL - (long long )hi) - (long long )lo >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5dd47802-dcb7-40ac-bf18-3f4e5b300147
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 33
    column: 8
    function: main
  location_invariant:
    string: (long long )hi - (long long )lo >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 52d7ad9e-015a-47ce-8600-0f28d8f02605
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 33
    column: 8
    function: main
  location_invariant:
    string: mid != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 247c2d7c-9459-455a-b827-31e14563d60a
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 35
    column: 4
    function: main
  location_invariant:
    string: 0 <= lo
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5644513c-0f84-4fe3-b651-34cca314de19
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 35
    column: 4
    function: main
  location_invariant:
    string: 1 <= hi
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c317f620-6f3e-4ad1-a303-a543c6cf7759
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 35
    column: 4
    function: main
  location_invariant:
    string: lo <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0ca02c13-bf96-4c3a-84fe-13504923bd1f
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 35
    column: 4
    function: main
  location_invariant:
    string: hi <= 2000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0f65e665-d659-4b27-9c73-5e4c18104085
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 35
    column: 4
    function: main
  location_invariant:
    string: (-2LL + (long long )hi) + (long long )lo >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 02cc0216-bd68-4fb1-aabf-9f80d51edcd1
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 35
    column: 4
    function: main
  location_invariant:
    string: (0LL - (long long )hi) + (long long )lo >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cbedc55d-7420-4b1f-b8db-c9683aa600f4
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 35
    column: 4
    function: main
  location_invariant:
    string: (2000000LL - (long long )hi) - (long long )lo >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 475f28be-a0c9-45a5-a04d-9c7936b87aa7
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 36
    column: 4
    function: main
  location_invariant:
    string: (-2LL + (long long )hi) + (long long )lo >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 786d5be5-b56f-46ab-a91f-ad9d3f032c83
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 36
    column: 4
    function: main
  location_invariant:
    string: (0LL - (long long )hi) + (long long )lo >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd2d9f16-7ce4-49c6-8bd7-d58959446690
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 36
    column: 4
    function: main
  location_invariant:
    string: (2000000LL - (long long )hi) - (long long )lo >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0bf75694-6640-4c32-91d7-68524b4f851d
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 28
    column: 8
    function: main
  location_invariant:
    string: 1 <= mid
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 69017778-605c-475c-a7e4-99a9050353e0
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 28
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )mid >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2416c6f6-fc49-4e55-81c6-54ec7ede2854
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 28
    column: 8
    function: main
  location_invariant:
    string: mid != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c20b2d7c-ce66-4e7e-99a4-6e04146ce08f
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 28
    column: 38
    function: main
  location_invariant:
    string: -1000001LL + (long long )mid >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9247c58d-2cf2-481d-9ab4-83ee68d0425f
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 28
    column: 38
    function: main
  location_invariant:
    string: 0LL - (long long )mid >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 31e8e81d-04f9-433f-96ef-421bf0e5d8de
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: 0 <= lo
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 715c980c-b4bf-4838-b626-e0baac87251d
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: 0 <= mid
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 510bf4c1-7597-437b-a03b-26c91e40bcf9
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: 1 <= hi
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a83fdfc8-b68f-42ab-9e4a-e6c4fc0c5626
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: lo <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9ec172b0-c19c-403b-b8ee-1316e4712997
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: mid <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 91bd7d9c-c3a9-4350-b404-c8a70dc85af9
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: hi <= 2000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 615603c3-4e29-4357-b5db-617f3a92b70d
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: (-2LL + (long long )hi) + (long long )lo >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4de004dc-bcf4-4e5b-8098-59df2be3188d
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: (2000000LL - (long long )hi) - (long long )lo >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4f338a3a-083e-4f16-843c-ec6cba04f472
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cggmp2005_variant.i'''
    task:
      input_files:
      - ../plain/cggmp2005_variant.i
      input_file_hashes:
        ../plain/cggmp2005_variant.i: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cggmp2005_variant.i
    file_hash: d63924edab54dab3adf6fc30d0dae54d46ed57e9ae48bc8d03de12421cfd3603
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: (long long )lo >= 0LL
    type: assertion
    format: C
