- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 08aa3e6c-664d-4002-b25c-551a4f6204fd
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: ca1a7150-1b6c-4e2a-b743-5e958cbc4861
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: d11db5d5-b0e7-415d-82cc-65177227fb10
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: 96228996-babc-460c-9ef1-49c5df6851a8
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: 093afec4-d584-4dee-bf3c-e86939e07127
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: c9e7b798-ecf3-4984-8c95-acd58e173b03
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: c589f69c-6c01-4655-b90f-ade2fcc879b5
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: 92573d23-b43f-42ee-a599-2fcabe413707
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: bb086ed1-450b-4a36-82fa-4dd2fd0bbdf3
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: f29f60ab-3d4c-4b36-b3c4-491816758991
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: 74fa3d91-c1b1-4418-99dd-97e26c69dfdb
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: 7cd10a45-4e05-40b3-9c48-498ee40ee98b
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: 141e7624-a562-4bcd-8daf-5fef9b693d5e
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: 41d35667-0825-4b7f-b480-a5ef0b57b3cf
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: c429bc50-c32a-4dd4-8836-5500dab625a6
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: c02d5ab4-75e5-4e9c-8b7a-34abfd297f3d
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: 6779b600-e731-4713-9157-5ede6baf1970
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: b265ce13-3e0c-498e-895d-b2b24512f199
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: 87e3e84e-d2b5-4120-b03f-929a6ea114a3
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: e566cf05-1962-419e-9d02-734b7eb1a5ff
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: 9d6fee72-6708-487f-a087-74f24cca806b
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: 97a00653-ef0b-41c8-9852-7d9be79d7ed9
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: e40e4cb4-c7bb-42bd-932f-7bac3b6dc8f7
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: 248ee4d3-0a31-41de-96ed-6b71f91bdea3
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: 436d07f1-eb0d-4bb3-a652-5b074be9443e
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: decc582b-2afa-46d5-994f-b7aedc297024
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: 7b2d0d48-e5d3-430b-b3e2-3c3c859e548a
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: e6e46bb2-8738-466e-8246-6a89be2cab57
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: 2e3fd0fb-4c58-463e-9c25-6e7b758d8cd5
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: 50db437a-609a-430b-814a-c3755c0d7c9c
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: bf0a4350-8669-4b81-98ee-8006d10cbd4a
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: d3ad1d44-3461-439a-97b1-6ecd9c814848
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: 00c580c6-1c19-450c-bc38-51a4c9dab95e
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: 469957a3-ac27-4a66-99b7-b32182d754b6
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: d7e5f009-4a01-4dd0-8c3a-c49e1e8a3e19
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: d242253c-c751-411a-a9b3-f51295acb89a
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    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: 4f6911ef-343d-4c29-b5d6-2032cbaa6ff5
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound1.c: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound1.c
    file_hash: 4d98b743606513f831b0c11a7a0f14d9c6aeb2efbb7fa03be80b69c46d40fb39
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
