- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c65f1660-a5fc-4760-8ca0-af6da57240bd
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 35
    column: 8
    function: main
  location_invariant:
    string: -4611686016279904256LL <= az
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a6477b84-33d0-4616-bd15-4e47242c1e60
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 35
    column: 8
    function: main
  location_invariant:
    string: az <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bc0f451a-3415-4efd-a009-24065b2cb959
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 35
    column: 8
    function: main
  location_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ba2bbd16-f55b-4484-b3d7-c3cd64ac25e6
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 37
    column: 12
    function: main
  location_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82063bba-c52e-4474-9900-f9be8388a624
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 37
    column: 12
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ac05c83-aeb0-4f78-b6c4-bd7926a2e337
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 37
    column: 12
    function: main
  location_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b2471182-788e-4f7d-9136-d262586fee47
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 40
    column: 8
    function: main
  location_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c8edb180-513a-437f-a70f-a7aef5a95b42
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 40
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43d841d1-a92b-49fe-a97d-f864616e7aad
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 40
    column: 8
    function: main
  location_invariant:
    string: (-1LL - c) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8d7742d3-5c7e-4277-a563-b251dae72c3a
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 40
    column: 8
    function: main
  location_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a36dea9c-474c-4aee-8bb6-2404a8c2ba9e
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 2LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8284118d-6559-47e9-8c4e-60d96930d4e3
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 41
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b7f4849-7be1-488a-8c8d-dcc45afe79b8
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 41
    column: 8
    function: main
  location_invariant:
    string: (0LL - c) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a05717d5-21c7-456d-835b-5e8d6ad3534f
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 136e2d5f-cd9d-406e-bc81-efd2e2a49847
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 42
    column: 8
    function: main
  location_invariant:
    string: (0LL - c) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 12b4b835-3d71-4f4b-bc5d-772ee73af2fe
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 42
    column: 8
    function: main
  location_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 39fae93f-1c9b-45ff-910b-0a66ddc6fcdf
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 44
    column: 4
    function: main
  location_invariant:
    string: -4611686016279904256LL <= az
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 65e6be07-fd9f-4202-a99c-2b55a7cfcfb1
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 44
    column: 4
    function: main
  location_invariant:
    string: az <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a7d1ba2c-d182-46b5-808a-882c83861c9d
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 30
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: be902b75-0143-48bf-8f9f-bfe3bcccfe17
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 30
    column: 4
    function: main
  location_invariant:
    string: x <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: dbc6a9d5-caab-4dc4-8630-50c15bd7051d
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: -4611686016279904256LL <= az
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 39b512a3-fb04-4720-baf4-955a053ad485
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 0 <= counter
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7583f4bf-5f43-462e-916b-fbdd753a2fc1
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e5fd8aa-61a0-4493-9f8a-7ccff629c35f
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: counter <= 21
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 76091a6e-f381-4898-992c-e14bf55b86d2
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 320b9c0d-5ec9-4ce5-9582-329b82647f04
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: az <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 12cc09fd-031b-4d2a-aa28-23f6178bb95a
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound20.c: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound20.c
    file_hash: 8da870150b2997ed8b5b2bd7f8bc29b32b30f67a033bb6d7b4e930c9ba2a33c8
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
