- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c310fc91-a87f-486b-b21f-1f697651da8f
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: e6fd7e41-c72b-40f2-9e46-f2117ba210df
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: 74e32ecd-adb9-4a55-8cdb-f62a8e92c10c
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: 726195de-e90a-4c58-9d7d-ce5582a6fb0e
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: 28e32daa-79d2-4164-957b-72a645fe3a22
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: de906a0b-d63a-476c-8d76-c1dbfc12512e
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: 94316a61-84c3-40c5-b882-4b4f8229ac63
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: ca5a1922-5709-4c3b-be16-a47f04495009
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: e85a67a9-dcfc-41dd-a76d-913130c032fd
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: 70476013-1a6e-4ed2-b830-13b56cfea041
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: 053ea363-ca7f-4d69-8fc1-b6743ec9401d
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: 1733106b-39ea-407d-99f5-59e4ec12b28c
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: 492c67dd-f895-435e-afcb-b5c7fded6a61
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: 1847f092-08d3-4675-b932-0064a4364011
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: c96a94b0-4472-4eff-bf59-cb3cf0371a3f
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: 67e09712-c132-4681-9395-e0827611ea8e
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: 6ad2711d-14de-44cd-9b40-413ebec9b46c
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: dd4e8a80-b7d3-4c44-99bc-35c777839850
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: 86e73b7d-8370-4c01-a20f-3adbcffe0807
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: 63bcccd1-23ed-4460-ae76-649d62c09ca1
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: a258acd5-8402-4a7e-8675-85aac6c9ef31
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: 257ddacc-aa17-4c80-8582-e9f6d3a9d293
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: 03c222e5-0b5c-408e-9e09-38c92d54ec4a
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: 0d9918a9-4720-48c9-9c82-890cba2342d9
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: a197c417-f00e-4be6-85b5-7067b3701de1
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: dc71811a-013f-43b1-847d-b882669cb3a1
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: fc8138ab-19df-4f5d-8d1a-e30fec968e55
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: 5c04b144-91b8-4b8c-b7eb-58a840b39c40
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: 99e2bb99-79f6-442d-89c8-916381bb517e
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: 88322888-1c89-42b9-ba56-5a8b528815c1
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: a395b574-bbb1-498e-a966-73711831f754
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: d339f7a4-f683-4897-9976-c46544827f98
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: f11ed2be-2c50-442d-a59c-c85aee8ce07f
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: ad17ff59-100d-44c5-999a-f05819ada68b
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: aad9733e-2adc-4360-81fc-7f3d82b5a45a
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: f415ed92-2237-446c-97d2-f92d0acb8c33
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    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: d83292b6-96f4-4e27-8e39-6a25cd0f22ba
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound10.c: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound10.c
    file_hash: 69ffbc0bd4f07a8cc2897410fc013fb815dd984602255263415f4f8a1a4c1714
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
