- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b416887-c52b-4be2-9963-1a8afd7d04e4
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 36f1e288-fbe6-4b24-98b1-c4563e94676e
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: ead4d4b5-b097-4a13-8c13-34590acb3165
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 8508c52b-22a7-485e-856c-1ba01b240fb1
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: c5853f5e-e70c-424c-acfb-7009b64b7ec7
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    line: 38
    column: 1
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a4fc520f-40f6-43ef-afa6-f504ea275cf9
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 9793d616-5481-4764-bb41-63dac581258c
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 8c477418-5f1e-419f-8fdd-ae6beda8cc2e
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 1ed24867-c891-47a1-b589-8bb5e6e4132b
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: a2fd05b3-0fc6-4d7e-9519-e93a4ed8f7db
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    line: 39
    column: 1
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c9359a4-2054-435c-81c2-2c7bb75c4b10
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 9108a326-c27e-4ffd-9da3-106fa47321ce
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 95ea9e34-8fbd-4c3e-b005-46bf7ff74b34
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 2361673c-f80b-492d-8d72-52f5e7799f52
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    line: 41
    column: 5
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4d37d54d-f4ef-41c3-bc34-ad59a5afba97
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: d3b006e9-e412-490d-9a0b-3789cf34a915
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 9dd8c83a-d34f-419c-93c7-495fac54c7b0
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: e2a33fae-5c24-4b9f-8a03-e2c069929b30
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    line: 43
    column: 1
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bc15b5ad-49bd-41cc-bc6c-6cb8f2ee9aae
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 5506d29f-29f9-44f7-ae81-97df58370613
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 5050adf2-469b-46c1-870d-d9f282854681
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: f42a7a88-d15a-4445-9aa7-3f7bc293c9df
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    line: 44
    column: 1
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 311eb6be-9a47-482d-8e77-60096cbd807a
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 5c9bb704-33fd-44d4-bb61-6a5383d9049e
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: d8916ddc-0dc1-48d8-8fbb-0fae54e64145
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: ebe5dcaa-fac1-4a7c-b15e-a642274787f0
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: e1c34735-35c0-4df2-8051-d245dd0da098
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: c759ee16-fec9-421d-8799-a49d53943c73
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: b783dddc-7ada-4c58-939e-29f4e0f2a09c
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    line: 47
    column: 5
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b904a09-e574-4ed6-819f-69855459ec31
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 55a4ed5d-bb66-4abc-978f-58a91447ca67
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 9b9543cc-2c78-456c-8208-9b5de12b8da8
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 831bd273-95a2-4a7d-87dc-ff6b146616bd
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: d1b64e81-f435-4b40-9175-2a1f056225ce
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 960e64bd-b6da-4ea5-88dc-449b2103077f
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 722e31f3-9d0b-49e8-9da0-8491f44fc699
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: e017be0c-9faf-42c1-bc19-0d04b79f3005
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    line: 48
    column: 5
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ac2b6fbe-ca03-43be-a67e-4ac0e5a8177a
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 5b025b9a-199c-4491-822e-470630949f87
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: c94089ab-3129-44d2-ae92-5f3a561dd6a1
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 505e74a4-f3d8-4b93-9056-4427319e9a53
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 5523fcca-e997-4faa-802d-64a4b5cb6b5c
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 572f33be-4436-4c79-b5a7-4a12fb389e5f
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: bb20711a-c111-423c-8ba7-032793b0dfa2
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    line: 49
    column: 5
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e13013e7-f690-4ce2-a58e-c6a133a93efe
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 37967683-f763-4c4c-8c0e-6e53b4623bd5
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 46d05637-fc7f-438a-8994-5d1a4b94e8ca
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 8d6ba26a-c2ab-47a9-8b03-a5bbe403c9ba
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 2a88e616-fa36-476b-b2c3-804b8df32275
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: f961674b-3a0d-42aa-a4ef-585ad797bb1a
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: a6e3dd8a-623c-4aac-8a89-f00fe5e372d5
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    line: 51
    column: 9
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8b5c32e8-894f-4f1e-bc4e-a8783f0ce707
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 92f82713-baee-43e1-a329-e42a4a2986a7
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 2dfac045-b0d8-4fcd-ac69-f6c1fedd4e44
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 6edbdb35-49f8-474f-b2a1-3a9d56310e30
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 04a610e2-58f8-473b-b7c9-d35b230285d5
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: e9b0393b-db41-42d4-9670-aaee3d5334ba
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: bea525b1-58b2-4976-a81e-ad22993c720a
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 7373e903-bbd3-48bf-afbd-938e0ee8fd04
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: b62ff232-f4f7-40b7-8273-5914f7e9f473
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    line: 54
    column: 5
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 42a677b0-15e9-43ed-bc38-519378d25871
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: ba132693-084d-448b-82e2-e840aeb7c5f8
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 1d3288d0-3a89-443b-be29-ea3db0b6d545
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: c6b237c0-5f14-49a1-ad82-969968d6a240
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 9b045bb5-23c2-43de-a524-ca90bc71db52
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 73e06ff4-78ea-4988-a395-3249ca8a1b27
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 051aec3b-ff6f-49d0-bbde-bc455c53244e
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 4b222ef4-ee67-4a72-8a79-f784203c7c68
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    line: 56
    column: 5
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 819ef6d2-8a3a-4832-bd59-367ac226b3ba
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 47b983e5-6d0b-4b68-981d-a82a917e976d
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 58703ac5-f852-436b-9697-1bf51bb48630
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 2df96f24-f658-4ce7-96b1-3b0c0e05a03b
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: c93a588e-2239-43c5-9ce1-58168d742355
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 3e80b025-5db7-4918-a918-529329ae4666
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 4b1bff55-fe0a-4589-850d-d1b6c10c1b03
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 45bfab03-dd45-46b1-b092-d500da19fbe3
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    line: 57
    column: 5
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 064eda50-e924-425e-a68e-85c461a60c43
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 984a3964-f8df-40f1-b8d4-152b0e8f3b5c
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: e15dadaa-29c0-4b05-ae9c-3061029588f5
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: bff31a1c-0beb-4d51-a6b6-ed7eda7845e4
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: a41f5a2b-890a-4bb9-bd1b-b3bd9e4f4d2f
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 7773a909-b8fe-4763-9c74-6194ae898c0a
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 31dde640-4433-463c-b89b-60639c8a649d
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: d57d3e37-6d72-472f-adda-3803628a6a63
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 67dcdd12-bb64-4fb6-9541-1296c5deaa68
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: e4103b06-f225-4aa7-8318-bcfb77fa82dd
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 94a3aaa4-fc9f-48d4-ab1b-e0cdf5ccaf82
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 677d51b8-5cce-4956-be46-8442d607a2f1
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 2655a09d-d5c6-4b2d-ae19-4963a9ef92f8
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 4ffbd294-a7fe-4249-9509-a396dccd9e57
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 0f57ce69-e7c8-4c54-a671-52251c8bdca9
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 5788c51a-9a45-41ad-970d-d963b70b4ca7
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: f6509196-5ba9-4311-b571-016eca696000
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: e35fadc2-c184-49d8-a2f7-2ed5e20ec173
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 786fae4a-c212-4ad6-88af-ff307bd3c50c
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: f2d4955c-b637-4c50-88e9-10d8ce815245
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 8d68011a-49f4-400f-9000-8548e94cb7f9
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 754d88ff-8465-48db-bdb5-258b03a6073a
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: ca24c3a2-ad5f-43df-b2a1-2d5c470921bc
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 8755d473-3574-4dfc-97da-cd43a11e57db
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 0a6f0005-17ad-4d8d-bfcb-b5618ccdbdd2
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: d1637161-bc5e-4da3-b227-8a8e059c9878
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 9acdfe9f-0247-4ec0-b856-cd6fb7908890
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 994a0404-a931-490a-8df6-6645808ffd03
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: fa997fa0-e647-456b-b5a5-8ead843c20bb
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 8e2b88e6-17e7-4145-86e5-732356a117ae
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: counter <= 101
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 41b05c64-2538-4359-a500-be699a37a7d1
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 503b9bdb-ac65-4a68-8dbc-e3ed10d749ff
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: 101LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 17c6e78d-5264-4064-8bb8-6c545a7378f1
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: 101LL * a - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 57b58144-f863-46ca-bb4a-5f623d707c3c
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 9159ae67-cff3-4c97-8dc1-15c546ad0860
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 212a3799-4235-4578-91e3-9ca57141da28
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: dc1133c0-6cbb-461e-954d-c2ea055a0213
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 309f05e8-3de2-40b7-8303-33cc737473a1
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: e1491317-6f19-4199-8d48-cbaa38fc405e
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: counter <= 102
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d8be211-9cc9-4eb5-8b9d-f283cf9b8bf8
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 0168f17f-7195-4dad-83b4-67b717b7e2f4
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 4d106096-4f6f-4ce4-9a42-f3e57dd45643
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 3364d6ba-be98-492e-9429-9f145e992f05
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    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: 1ed97ebd-f169-4449-acf6-4e065ea62e65
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b6561730-4277-42ee-9cb9-7801863b0f75
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound100.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound100.c: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound100.c
    file_hash: 7cdbf1a1c8f20bea42ab4ad35fbada62352deeb8460cfeb3778e870071fb234e
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: r - (long long )y >= 0LL
    type: assertion
    format: C
