- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 83ac0e50-e8f8-4000-bec9-7a176bb3fd67
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 35
    column: 8
    function: main
  location_invariant:
    string: -4611686016279904256LL <= az
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b773bb4a-6299-430b-94b6-93a0749a4fbc
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 35
    column: 8
    function: main
  location_invariant:
    string: az <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f1eb9ad0-0807-421a-81e4-06e1041bb8b5
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 37
    column: 12
    function: main
  location_invariant:
    string: 0LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: efb7ab78-07e2-46d9-aade-febf73f2f75b
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 37
    column: 12
    function: main
  location_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d471c13a-62a5-46f5-a4a4-08ca7b98e43f
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 37
    column: 12
    function: main
  location_invariant:
    string: c <= 2LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d6da2a37-85e0-4e41-a7d9-52eb610792a9
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 37
    column: 12
    function: main
  location_invariant:
    string: c <= 127LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1d0a4f1f-72d2-421a-8512-37e5e242165c
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 37
    column: 12
    function: main
  location_invariant:
    string: c != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e145b51b-63cc-4817-a862-d1fc2309b91c
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 40
    column: 8
    function: main
  location_invariant:
    string: -2LL + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9fe52f91-a67e-421b-8074-5f7b5a0309df
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 41
    column: 8
    function: main
  location_invariant:
    string: -2LL + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bb0e68da-77d6-49da-99b4-deb14c90baf0
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 42
    column: 8
    function: main
  location_invariant:
    string: -2LL + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 33a8597b-0b26-4f58-8171-2df184078275
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 44
    column: 4
    function: main
  location_invariant:
    string: -4611686016279904256LL <= az
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 72eca526-c323-4256-ad4e-5b4d4406e5c9
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 44
    column: 4
    function: main
  location_invariant:
    string: az <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 461d5778-6ce8-4c20-9728-66c386d13c9f
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 44
    column: 4
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0848dda2-4ebc-4235-a947-d3fa66ecbad9
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 45
    column: 4
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4d4a702-ed11-465d-8d85-7dc4e7515cb6
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 45
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e650cfec-700d-4ac1-8d1c-dfae30779f8c
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 15
    column: 8
    function: __VERIFIER_assert
  location_invariant:
    string: -1LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 80cb1c53-2d3a-47cd-b6e4-7853d3347e2e
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 17
    column: 9
    function: __VERIFIER_assert
  location_invariant:
    string: -1LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8b7f1090-5e78-433e-a7d5-5a51319e68a0
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 19
    column: 4
    function: __VERIFIER_assert
  location_invariant:
    string: -1LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de0fd455-8023-4f7b-b5ce-b90a4c6f71a3
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 30
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d4847288-ee5b-45bd-93c2-1ba6a1d61046
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 30
    column: 4
    function: main
  location_invariant:
    string: x <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ce8ed82-4c7e-41d8-9fa1-f016d20d79d8
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: -4611686016279904256LL <= az
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b5ec262-5cf5-4044-abe2-3aaaa1e631a6
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 0 <= counter
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0979cdb7-8e40-4293-b47b-950f297f459d
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c34bfa09-ecf8-49bb-8a86-de0d5c2c7cd0
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 81e82589-5e90-4176-98c7-f66735a6b025
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: counter <= 2
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 307875d5-7184-43e3-9273-d98faa6d0258
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: c <= 2LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fe96c965-59fb-4649-8f69-5d7dd267a25e
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: c <= 127LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f9a360eb-8bfc-4038-9741-6e87b56f10d0
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: az <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ce254992-d745-4be4-8963-9bd8ac3383c9
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 16ad2705-cc1d-466a-afba-b2c3d24d7fff
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 2LL - c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4655530b-d781-413d-8421-ac2f69cd6d7b
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound1.c: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound1.c
    file_hash: 91c207b4b9ec9497b682edea4de56d410c70b882e6c03e91b56844bba1af20ff
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: c != 0LL
    type: assertion
    format: C
