- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5161dbd9-d8ef-452e-a48a-84944fe7b763
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 38
    column: 1
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ba265fc7-a569-4ff4-a241-0362d3b97861
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 38
    column: 1
    function: main
  location_invariant:
    string: 0LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 76667d15-a200-4028-8d10-93ae40e05154
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 38
    column: 1
    function: main
  location_invariant:
    string: a <= 1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a67d7a0-8ac8-4b03-a6c9-490c6fdb184a
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 38
    column: 1
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 08a940fd-00de-4ef5-a29e-38f3e2f13165
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 39
    column: 1
    function: main
  location_invariant:
    string: -4294967295LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7947839b-1aa3-4e23-b2aa-bbbabeb9292a
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 39
    column: 1
    function: main
  location_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8998a291-5020-4b30-a9a9-c75d59685508
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 39
    column: 1
    function: main
  location_invariant:
    string: q <= 1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3cb9031b-1179-4855-b57f-ed92eaaa56f8
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 41
    column: 5
    function: main
  location_invariant:
    string: -4294967295LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b051c627-4393-49d6-a531-3dfb4a408e61
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 43
    column: 1
    function: main
  location_invariant:
    string: r - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 02bb1cd1-7ffa-47ef-bfa0-447a06d4e1a0
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 44
    column: 1
    function: main
  location_invariant:
    string: r - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d32a2178-33d5-48f8-9dfe-4ae616932927
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 59
    column: 1
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 80c6483c-2073-45d7-a3a4-27b0f9a26022
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 59
    column: 1
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: da505649-3e0c-4076-9d92-23a57c81d0ba
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 59
    column: 1
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c76edc49-5b04-4f49-a621-0cffbfcddf3e
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 59
    column: 1
    function: main
  location_invariant:
    string: (0LL - b) + r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d25f435d-dc8e-4437-af0c-dde7a0181595
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 60
    column: 1
    function: main
  location_invariant:
    string: -4294967295LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 980a3fe4-bbfa-40b5-8a1e-33e38336b36b
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 60
    column: 1
    function: main
  location_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 57e8c257-45c4-48b2-bbdd-90b0bd042141
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 60
    column: 1
    function: main
  location_invariant:
    string: q <= 1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b2bf160c-1769-4860-bfc9-3a29fe8ff401
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 60
    column: 1
    function: main
  location_invariant:
    string: r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9bdb3ef1-61cf-4498-85bd-f9fa7ccef874
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 63
    column: 4
    function: main
  location_invariant:
    string: -4294967295LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 740c6cea-b16f-450d-a48d-41366c4c8821
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 63
    column: 4
    function: main
  location_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: faf92294-df3d-4f4d-837d-d39a12b1e141
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 63
    column: 4
    function: main
  location_invariant:
    string: q <= 1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ebbfdc14-3e14-4eda-8eba-459d35c617ab
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 63
    column: 4
    function: main
  location_invariant:
    string: a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 39328a8d-0836-4b1d-abea-eb55d73324e0
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 64
    column: 4
    function: main
  location_invariant:
    string: a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e591e0f3-fd22-4b84-a5a9-8c0946bcf3b8
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 64
    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: c670def1-3643-464b-ba83-db787dc7c6bb
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    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: c1d430d3-e8fa-420a-a5be-4c042e5a4201
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 17
    column: 2
    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: 1a2c0bf6-b51d-4944-a9fe-7031010a4b7e
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    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: 3e2a1b3e-05a1-45c3-991b-a57b784abe76
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 34
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c66ac141-49f3-490c-aad2-7046e87b45d9
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 34
    column: 4
    function: main
  location_invariant:
    string: r <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a4bb7ee0-f3af-428d-91bb-1c83265bf2ba
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: -4294967295LL <= r
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ec5a1b6-224e-4a10-9ac4-848aef27079f
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: (-0x7FFFFFFF-1) <= b
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bcb5f75c-b46e-491f-a666-ce95d0fdee6f
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: 0 <= counter
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 37c1e435-6a1f-42d3-9770-63d2333744ac
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7cb07cd6-3251-4746-b1ef-8c07f3d89c58
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b90831bc-68e4-4ed7-bff2-7f0e182d2ea1
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: counter <= 2
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 214a148e-f2c1-4736-8d77-8b0739e461e2
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: counter <= 127
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: be8fda30-ae9c-48ce-8fe0-9a16f2decbf0
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: q <= 1LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0fcb9eae-6b15-42ac-a2b2-df5767d8ed4e
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: a <= 1LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 169acd73-c685-4804-9b86-c436e9ad7caa
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0b1776c9-f96f-43ef-8104-c296d70857cc
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: a >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 401409a2-fce0-4841-a024-017219dbfdd2
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: 1LL - a >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 926653c4-6c62-4aab-92b6-46c366b315d8
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: (-0x7FFFFFFF-1) <= r
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 199827fe-4349-4e3c-9f14-6b5fb198f961
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: (-0x7FFFFFFF-1) <= b
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 01b21443-35be-4986-a9dc-7886e616a013
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: 0 <= counter
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4dff6cf3-cc1e-4ed1-bab5-121e799db741
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 26b3b8c6-7f5a-4d91-92ec-effe1cefd278
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: 1 <= counter
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 881623d5-06cb-43d2-8673-6c4e5de5e3fb
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: counter <= 3
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b162b1be-14f0-428d-994d-fdc4a8258457
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: counter <= 255
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 29a316c0-033d-4cbb-b1f6-28877b435400
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: q <= 1LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0efc5e78-789a-4f4c-95bb-82bbc526e690
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a42a030d-f9dc-4de2-9fd1-e06a8d1b6245
    creation_time: 2023-01-27T16:29:19Z
    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/cohendiv-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound1.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound1.c: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound1.c
    file_hash: 079768eb2ce141267a1411f9330cb4d0cef674bf78865555f3130b47379d643a
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: (0LL - b) + r >= 0LL
    type: assertion
    format: C
