- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1301a1d9-4dcd-4ea3-a59b-ca30a8ab4c08
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 27
    column: 4
    function: main
  location_invariant:
    string: 0 <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e136a18-7b44-4faa-9a07-7aa864d2dda0
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 27
    column: 4
    function: main
  location_invariant:
    string: (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ebebd627-dc1d-4374-b599-3ca06ea683ab
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 91729cbb-1593-4027-a052-895e662ae0ec
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 68773e47-7aee-4c10-a55d-3d9f9f62a882
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c4bab933-9a6a-4723-929f-c04984982101
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 32
    column: 4
    function: main
  location_invariant:
    string: x <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 51fb3105-be10-4df4-a12c-a663347c534f
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 37
    column: 8
    function: main
  location_invariant:
    string: -4611686016279904256LL <= az
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cc5f5d14-da34-4d10-b0a3-b702ac77fc89
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 37
    column: 8
    function: main
  location_invariant:
    string: az <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 477ed400-60ef-4302-96fe-b75d31f26ab5
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 37
    column: 8
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 569706d5-f83b-4f5c-9612-03a2bb2931ad
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 39
    column: 12
    function: main
  location_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3b1ded51-d8a4-4f2a-81a9-73de30b7b155
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 39
    column: 12
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ac837a92-0887-4ae4-bd35-3560476ca68c
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 39
    column: 12
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8314f558-7676-4fac-97c5-8aae917834d5
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 42
    column: 8
    function: main
  location_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4d3b64f2-3b7b-4582-b273-71bb115e9857
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 42
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8dfc4ef2-9367-4f37-94b2-784964e2561e
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 42
    column: 8
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ce2c33af-11f5-4dd7-b455-79f8b1655e3e
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 42
    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: 0a682173-b757-477b-9277-656d2d0c1132
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 42
    column: 8
    function: main
  location_invariant:
    string: c != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f25050c7-418b-4476-8c35-2d576ab1b396
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 43
    column: 8
    function: main
  location_invariant:
    string: 2LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 73ec978d-ee29-4b60-9019-2ec971029e1b
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 43
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c533c66-9b53-47fb-9c39-33d8a46339c7
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 43
    column: 8
    function: main
  location_invariant:
    string: -2LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eeeee75f-f58a-4949-95a6-6ae06da27011
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 43
    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: 923b5d1c-05d8-41d9-bfba-68ad8630b207
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 43
    column: 8
    function: main
  location_invariant:
    string: c != 1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 05c27d91-70a8-426d-a4ed-8cf1bed127ba
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 44
    column: 8
    function: main
  location_invariant:
    string: -2LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ae463749-c7c6-456e-ac07-1623c7a5803f
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 44
    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: 0fd25d63-2813-4028-ad62-9b1f2b8c55c9
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 46
    column: 4
    function: main
  location_invariant:
    string: -4611686016279904256LL <= az
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e187a69-e7a3-49a3-ab4d-cc489e152bc3
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 46
    column: 4
    function: main
  location_invariant:
    string: az <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 08f4859f-00dd-482c-9e4b-043f58d03eac
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 46
    column: 4
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8e796bf2-f2b4-418e-947c-3d3fe874b8b8
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 46
    column: 4
    function: main
  location_invariant:
    string: c - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b58d4d2-0309-4c01-9ea6-d5c5573e9655
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 47
    column: 4
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 95a6de3e-3561-4eb1-a5e0-f4307918b4e2
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 47
    column: 4
    function: main
  location_invariant:
    string: c - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f192557c-6db1-4858-9c62-460407ff3ff2
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 0 <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 50b8cb69-0d05-43ac-af8d-0e98bb6eb3af
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cafe3024-f95d-4665-a8bb-45dbd134ea5f
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: -4611686016279904256LL <= az
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c6e2326-ea13-4171-a6e0-417c3b0f5fa2
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6fffa9de-1f9b-4e4a-980b-1f2b6d7b5297
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d2729f8-cef1-487c-9b97-fcc40b818542
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: az <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b6fa4a56-7af9-4d32-94bb-7db3005c26ca
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound100.c: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound100.c
    file_hash: eca9698a1815aa69bf5bb4e6a29e6765cf3c81610416c113408762dc59e2dc60
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
