- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 59770852-ebf1-4b5f-9b8a-28baa0a72ce3
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    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: 3786e5b1-5631-4365-9449-03505895bc82
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 38
    column: 1
    function: main
  location_invariant:
    string: a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 860986c3-e42c-4ddb-a149-69badfff86e5
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 38
    column: 1
    function: main
  location_invariant:
    string: -1LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fe5bd54b-24d3-4e06-a924-70652fdb4537
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 38
    column: 1
    function: main
  location_invariant:
    string: (0LL - a) + q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b3e56af5-cdd9-4f0e-9323-ff92d0d45d39
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 38
    column: 1
    function: main
  location_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d31814e-f74c-4efe-801d-0ec994535d83
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    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: 9fe7530a-f7e9-4c00-bcb0-62c07fc3fbba
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 39
    column: 1
    function: main
  location_invariant:
    string: a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bc9345e6-4f79-4340-8c63-fad2c443ffc2
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 39
    column: 1
    function: main
  location_invariant:
    string: -1LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5436fdeb-9e3f-40f6-badb-0e908754398a
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 39
    column: 1
    function: main
  location_invariant:
    string: (0LL - a) + q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 775bc1bd-c00f-478b-8bbb-4e8296ec0504
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 39
    column: 1
    function: main
  location_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44d1e9b5-ea9b-4513-945f-a2bc8de93b01
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 41
    column: 5
    function: main
  location_invariant:
    string: a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b0b090bc-1c73-4fa0-a981-75a0beb5fe77
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 41
    column: 5
    function: main
  location_invariant:
    string: -1LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8d09d03f-3e85-4879-8040-ed5608f86602
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 41
    column: 5
    function: main
  location_invariant:
    string: (0LL - a) + q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 97c4c189-7872-49b1-8499-e2e542fa58aa
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 41
    column: 5
    function: main
  location_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f21e70a0-5ad0-45fd-a9c2-af5e0bead5be
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 43
    column: 1
    function: main
  location_invariant:
    string: a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc6fdf59-299b-4ac4-9be3-0e258c23cdcf
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 43
    column: 1
    function: main
  location_invariant:
    string: -1LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8135948d-c836-4ab3-8508-aad7f3f5fd10
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 43
    column: 1
    function: main
  location_invariant:
    string: (0LL - a) + q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d8e874cc-a77a-4eda-9bcc-d56d01399779
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 43
    column: 1
    function: main
  location_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b80be984-5949-4b85-b5a1-7f3b053143cb
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    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: ad383c82-6301-4e74-a354-814821370bcd
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 44
    column: 1
    function: main
  location_invariant:
    string: q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d2055bb0-df7f-472e-8116-1f98599c7a0f
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 44
    column: 1
    function: main
  location_invariant:
    string: -1LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 26904993-5a7b-4572-9f88-3d7371f8638d
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 44
    column: 1
    function: main
  location_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d800534-5207-4541-a34a-ac6bc75fcf6b
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    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: 8b1aa403-27fa-4845-afe8-672cd5cddb03
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 47
    column: 5
    function: main
  location_invariant:
    string: 1LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 283eb355-845b-4337-b0f3-2b65e47983af
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 47
    column: 5
    function: main
  location_invariant:
    string: q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 35ea0267-930c-4d6b-b726-b1c85f6b25e0
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 47
    column: 5
    function: main
  location_invariant:
    string: -2LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de3c4e2e-2ff6-4679-a2c3-8e59a2425a29
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 47
    column: 5
    function: main
  location_invariant:
    string: -1LL + a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 054591b6-5880-4644-ab63-25327c336582
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 47
    column: 5
    function: main
  location_invariant:
    string: (0LL - b) + r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3376b958-2880-4f0b-901f-ddb04be5fd40
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 47
    column: 5
    function: main
  location_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8377821c-74ed-42a2-aec8-796fed9881a0
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 47
    column: 5
    function: main
  location_invariant:
    string: r - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 913cb4ad-a1b4-46ba-a6d8-dc79146373b1
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 48
    column: 5
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4fb525e8-c982-4595-aea9-2b01804d416f
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 48
    column: 5
    function: main
  location_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d70e05f-97c9-4fab-a6b7-33ec3487d02f
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 48
    column: 5
    function: main
  location_invariant:
    string: q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c7a91633-9798-4106-9aa3-2cb42a8503e8
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 48
    column: 5
    function: main
  location_invariant:
    string: -2LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd9c7052-9db3-41aa-be10-e849f4aa814f
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 48
    column: 5
    function: main
  location_invariant:
    string: -1LL + a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 217f04d7-fbdd-4a4b-8367-1907adf3f19c
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 48
    column: 5
    function: main
  location_invariant:
    string: (0LL - b) + r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a38a6302-d0c0-481d-9ec8-658e3848b0f4
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 48
    column: 5
    function: main
  location_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3eee367c-e41b-4750-988d-11eb4b6e45a9
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 48
    column: 5
    function: main
  location_invariant:
    string: r - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4cb4f90a-c960-47b0-bafa-eee0336761b7
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 49
    column: 5
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ffa54026-d296-4c36-a2b6-75a9ee11b06b
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 49
    column: 5
    function: main
  location_invariant:
    string: q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8b5f4f12-115e-4c07-a066-2d11fe80d194
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 49
    column: 5
    function: main
  location_invariant:
    string: -2LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 158c11df-20b9-4180-81d4-bac67b7c7d5e
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 49
    column: 5
    function: main
  location_invariant:
    string: -1LL + a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 40528995-54e6-4584-a679-ec2848b3eca7
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 49
    column: 5
    function: main
  location_invariant:
    string: (0LL - b) + r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd64da96-8500-4634-ad9c-4f4ec298be7b
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 49
    column: 5
    function: main
  location_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e537587-4b92-4d15-b16c-8d552574e51b
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 49
    column: 5
    function: main
  location_invariant:
    string: r - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5a54c449-43f4-40db-abe2-7e89aa20483e
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 51
    column: 9
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dceada65-5b2d-4f5c-9f78-771713210c9b
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 51
    column: 9
    function: main
  location_invariant:
    string: q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 741f6f33-5cd2-40f1-a0e8-1e010d036a70
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 51
    column: 9
    function: main
  location_invariant:
    string: -2LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a24c13bf-36a5-4cf1-8de1-f771c55a75f1
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 51
    column: 9
    function: main
  location_invariant:
    string: -1LL + a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d5caafe-2d3b-4143-8080-ef2ed0b6b079
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 51
    column: 9
    function: main
  location_invariant:
    string: (0LL - b) + r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9e21363e-250c-4aae-9001-08bd5a9ff790
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 51
    column: 9
    function: main
  location_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e7b8376-6522-4c60-91a9-21f4e0ff5e3f
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 51
    column: 9
    function: main
  location_invariant:
    string: r - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 59ca80bb-0b94-41e5-802f-e821f4f37771
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 54
    column: 5
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 56ed6d03-7455-4eca-a7d5-be2231d2e4b4
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 54
    column: 5
    function: main
  location_invariant:
    string: 1LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 63d55037-d213-48e1-89d2-f441a4902841
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 54
    column: 5
    function: main
  location_invariant:
    string: q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8d4487be-a73c-480b-929a-c89ea56312ec
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 54
    column: 5
    function: main
  location_invariant:
    string: -2LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0dceb0ef-642a-430c-8508-8b33ac281499
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 54
    column: 5
    function: main
  location_invariant:
    string: -1LL + a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ba7b25f8-d6b0-45c9-8bdd-997fbc42127c
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 54
    column: 5
    function: main
  location_invariant:
    string: (0LL - b) + r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ce5e9b8c-2653-479c-a1f4-b2f63ceb9364
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 54
    column: 5
    function: main
  location_invariant:
    string: (0LL - 2LL * b) + r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 32be1007-2413-48fa-8c55-4d329b199622
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 54
    column: 5
    function: main
  location_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14115e51-038c-4b7a-b952-0320a3abf21d
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 54
    column: 5
    function: main
  location_invariant:
    string: r - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf6286c0-6993-4a64-b8a9-44aff4679436
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 56
    column: 5
    function: main
  location_invariant:
    string: 1LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f676e6d-33d3-4e57-940e-4cf5e88a81eb
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 56
    column: 5
    function: main
  location_invariant:
    string: q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e638f75-87b9-43dd-a606-99fbd18df12d
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 56
    column: 5
    function: main
  location_invariant:
    string: -2LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d6952ea-d2f0-4665-affc-11c72585f1f1
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 56
    column: 5
    function: main
  location_invariant:
    string: -1LL + a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 113abb5d-9024-46ec-a2f6-073efadd5ddc
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 56
    column: 5
    function: main
  location_invariant:
    string: (0LL - b) + r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b676bbe-b89a-4253-ae9d-540bf866208f
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 56
    column: 5
    function: main
  location_invariant:
    string: (0LL - 2LL * b) + r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f6eb2dad-c7b0-4bce-9071-1e8b556dbc8d
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 56
    column: 5
    function: main
  location_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4fb2d369-3e1f-4139-8a11-6dc6ca8ef764
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 56
    column: 5
    function: main
  location_invariant:
    string: r - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5b4af0fd-89e2-4f01-a57c-6cc343849336
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 57
    column: 5
    function: main
  location_invariant:
    string: 2LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1eec5068-8d65-45e6-b328-3ea4972b6348
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 57
    column: 5
    function: main
  location_invariant:
    string: q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fa02fd6d-3d47-4dc3-afe2-27229ab33218
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 57
    column: 5
    function: main
  location_invariant:
    string: -2LL + a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 103ff0f0-d0fe-4036-9a62-dfff91bc8f2e
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 57
    column: 5
    function: main
  location_invariant:
    string: -2LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9af60468-1f01-4f0a-afd6-fcc35aa91041
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 57
    column: 5
    function: main
  location_invariant:
    string: (0LL - b) + r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2ef105c3-398d-4637-9745-b81be3faadf8
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 57
    column: 5
    function: main
  location_invariant:
    string: (0LL - 2LL * b) + r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4acec154-1de1-476f-ae86-f4dea1f1a435
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 57
    column: 5
    function: main
  location_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ac70b364-7c75-4165-9784-6d1b231cf173
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 57
    column: 5
    function: main
  location_invariant:
    string: r - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8bafd4a9-bb97-4eb1-9bda-9bc3da8e4a29
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    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: 180489b0-06a1-45b6-a142-1dd1b74c9f1f
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 59
    column: 1
    function: main
  location_invariant:
    string: q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ede0e80b-3524-4ea4-a930-6ee6a08ba9bf
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 59
    column: 1
    function: main
  location_invariant:
    string: -2LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 538bb210-7be8-40d6-8bb5-f9fe883cb219
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 59
    column: 1
    function: main
  location_invariant:
    string: -1LL + a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b8e41fbc-5b27-4653-8b46-1f101e2044ea
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    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: 9b382027-aefa-4838-905f-9d8a1e213b3b
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 59
    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: fdb28583-80d3-41e4-991d-77966c585609
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    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: de1f4f7f-238a-43cd-85dc-9d819dc6d5f8
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 60
    column: 1
    function: main
  location_invariant:
    string: 1LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d51039bd-1a76-4147-a57a-dca91369a299
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 60
    column: 1
    function: main
  location_invariant:
    string: q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f38ddab2-a893-4188-9f01-dda857ebafbe
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    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: 538aa62c-6195-4f2a-8de0-9471693bf491
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 60
    column: 1
    function: main
  location_invariant:
    string: -2LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c7992f51-f4b7-44e3-a488-96f8392ce447
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 60
    column: 1
    function: main
  location_invariant:
    string: -1LL + a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 553f00b7-b926-4b29-82c3-f0b0d5c31f8c
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 60
    column: 1
    function: main
  location_invariant:
    string: (b + r) - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 36ea8cea-5473-4b2f-8c54-f8c17d29345d
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    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: 3484c1dd-8b21-4f90-8dd0-6f3503195a2d
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    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: 617e7a9a-e901-4c08-bcef-b2941ffdfe41
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 63
    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: 47f77f76-38a1-4b5c-80c0-32c3feb59da4
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 63
    column: 4
    function: main
  location_invariant:
    string: (0LL - a) + q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3443b5a-1a03-4739-9e12-2f81f5ee4143
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    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: a467bac3-628a-4686-8096-c4c160b777ce
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    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: f99cc4f3-0403-4b3f-b1cf-4fe967616717
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 64
    column: 4
    function: main
  location_invariant:
    string: (0LL - a) + q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1debb9de-2c55-4f64-ae8d-fe4a285bdfc1
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    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: 9cb7029c-df0f-46c6-b9c9-968358ee7ab1
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    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: dbdb759a-eb37-4567-90c1-374ffa5eaa46
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    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: e9e3b28d-fe61-4582-99dd-f3f3e7f28281
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    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: 7b2d5d93-bc2d-4fec-a3b6-825a14eee8bd
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    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: a15294d3-28e6-4a89-a8d5-7275d2683595
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    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: d195fea9-d4bb-49f4-ac1b-08fcacfb456a
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    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: 2eb9f8ff-efa3-4bf8-869f-42a0c84c1ffd
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    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: 60f6ed2c-f678-46d0-b3fd-6602b7269a3d
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: counter <= 21
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4faedbb1-463d-4d13-8695-265d3eab5eb6
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: (0LL - a) + q >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 761e3f79-3260-4aba-808b-7ddc1ee4d82b
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: 21LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fba8506a-7fe9-4546-99b6-e4dcfdcd4c94
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: 21LL * a - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c94cc070-750e-4083-839e-527f74f6605e
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 094617be-a430-466e-8bb1-db3c9aa1570f
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    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: 11e153ef-f44f-4dba-b0d3-6cbae5599d38
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    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: 066b8ce3-6a09-4dae-b0fd-bf62a91443fc
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    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: 18095a3c-4725-4916-b208-d3285ee601b4
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: 1LL <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: adc170a8-7d0c-454c-919b-f14563e03768
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: counter <= 22
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8a4ddaab-3c64-4c6b-9615-5139679f9471
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: q >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c3549c30-3c90-4387-a9a2-976e6802c8d7
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: -1LL + a >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a8bd49c8-2791-49ff-9389-76141218059c
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: -1LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e57e082-9dec-469d-8df6-86851ca439d5
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: (0LL - b) + r >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 29a59290-8843-4886-93fd-09e705a177f2
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d2006225-377f-492a-881c-5fad0fe8a7c1
    creation_time: 2023-01-27T16:29:21Z
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound20.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound20.c: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound20.c
    file_hash: 93ad3f0e42b4c26a38d8e528f550b89aecdadec634fd1fe3b21f86af4528c655
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: r - (long long )y >= 0LL
    type: assertion
    format: C
