- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5a59f0d4-2fd6-425e-9f24-50ce1f3db41c
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: b0245602-41ec-4616-856a-020ba376e439
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 14269986-a898-4ab3-9707-3826c56877b5
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: fb57e65a-e55f-4f02-b26e-8d66b8abcaa7
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 7f449fa3-9fca-4e1d-a9e9-0a184e7df6c4
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    line: 38
    column: 1
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a09b4f8-bf36-4ce6-ae1b-300f62c008c6
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: d8988655-e21e-4f6d-9387-59d5a5df193d
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 7406a63d-b3bc-46a7-8a49-f29f92c681dc
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 55ed07a5-450c-4d97-99a8-ac2e685ac49d
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 6401e68f-c97c-4183-8b67-07ae6c08debf
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    line: 39
    column: 1
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 771e311e-4a8b-46e2-a925-0a667a410b94
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 3d1e7c27-398a-4149-9be4-86a83b6db77e
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: abea11e1-d972-4469-b44c-21782ad0c8df
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 2f63b6f7-ae3e-49f5-8dba-f4cb0e5b0548
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    line: 41
    column: 5
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 773451b2-d267-49c0-8fb3-991561580c10
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 31e2aa08-a1b0-4898-9ab2-8792b5849531
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 2bc9865d-de67-4f0f-b466-bbfd87ca6c40
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: d92c897f-009b-4e8b-b4c0-e31d8a66b778
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    line: 43
    column: 1
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3285dfd1-9dce-4a83-8f23-65fcdee70307
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 18cd8cda-a8c2-4e92-8257-eb1f234f9eac
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 7549750e-fecd-4238-a43a-6f7620a2f220
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 8a2e544e-2c36-4bfe-a1c6-ba082dc99f49
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    line: 44
    column: 1
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c74f1062-0211-47a1-aac2-eebaa128a306
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 152b0fbc-06fc-4ef2-824c-bcfceab3ee69
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: eedb4015-341e-4bc4-8858-c34632c01427
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 723b8cd6-9ff4-45a1-9e5c-5ca2b8433433
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: d98e1189-ea25-4ea3-bdb0-55c7eff31252
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 13eab1e4-0cbc-4563-8f92-f1f24e85706d
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 6376103f-50ab-41f3-abc2-f4b34c55681a
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    line: 47
    column: 5
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d58be3e1-c8dd-4740-8e2a-61ec2ba413f2
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: f43678cb-8403-43a8-ae8b-09d87b12c7de
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 7b70ec91-395a-4d00-bada-630a7dfe9cd9
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: bd61c61c-bb47-4f77-bfb1-e0aedd1e6339
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: f0a1468c-ecc2-4d98-80cf-aa0a341aaa55
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 8398d506-7d0c-4132-849d-67ebada899b6
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 64f6f3d5-bf01-43a1-9021-a1895c21fc52
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 922d7bd0-d66c-4379-91e1-5f4c444d09af
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    line: 48
    column: 5
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a6d3801-5b12-4c4e-baea-afc8c95725cf
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 9cc320ab-6e82-4680-bf4d-395f0066254b
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: c5af8b2f-f2f1-4772-89af-b74f1c00884e
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 78e16c65-61b3-444d-8fa7-6d1dc90bf69f
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 8bedb836-7bf7-4494-914b-0b699db3513b
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 69c30721-67d5-49ed-9db0-d07d5e5edf1d
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: be104ba5-2880-4269-8b0c-f3fac7ce3803
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    line: 49
    column: 5
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 18717b1e-b0e3-4243-a73e-2d8f81531e56
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: b2e3bacb-2c98-495f-8c8f-59635d60e3d2
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: f444c13c-a16e-450e-b583-54eb038f0d1c
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 8acd124c-c425-4ba7-965c-57e58f58854c
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: d4a88070-1e1a-4274-8451-85b17a28ba2d
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 7de1dc76-7fcd-4144-a176-b9ae0c592613
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 09b35e44-636d-4f94-ac5f-9b8d5a2d23d0
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    line: 51
    column: 9
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 87375c29-456e-4515-b9d4-0576586548fd
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 7bc0f928-c0b8-4fd8-96ec-797f2008423f
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 77df2eaf-34e8-4c2f-a875-f611bbb5b8ad
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 285d8388-d100-43dc-9e2a-0d591954d87d
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: bd9e0e8c-91c0-41c6-88bd-facef70cbf62
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: d0f66ee8-dff6-419d-8bf2-c610bdfb7e2d
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 1415e2c5-d8ca-463d-8ac8-c20ad8949174
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: dbca0ac4-841f-47d4-a61c-10bb7cd2076d
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 16e857f0-fd48-4425-8186-6dd9ef1ebbe8
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    line: 54
    column: 5
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a8ff18e-dc50-48dc-8447-ba8a3766882c
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: f5305a18-027c-470e-aef1-5b5b1828f0c7
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 469aa4f3-3bdd-48f1-8ab3-fc034b2c6aba
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: fced6743-d59a-4d98-9dc5-44a9e8ca5117
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: ff53bb8c-fff2-44ff-80f9-15e7d7c5662a
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 2acac3af-b958-4ec3-a228-567d9fc19c6d
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 6c8757b6-20b2-4650-819a-4bb43fc73a9a
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 592377d5-1051-41b0-a3f4-4213ae57cf45
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    line: 56
    column: 5
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 02dd0f0c-736f-472b-a304-a0028c919abf
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 4185fecb-7287-480a-83f2-aa424217b055
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 64ffc3f1-5104-43b1-9685-60c8e9348fc0
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 8eb9d8bc-a614-408d-b301-134860bc00cc
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 969e747f-89d3-45cf-b511-0e96b2739b07
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 90345358-5f54-42c9-bcc4-4dc53f6f8068
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: bb33fe4f-b2aa-4aa2-8438-b4dcec6a53a3
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 7a1374c7-84f1-4cca-b86c-9dfcc970a46c
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    line: 57
    column: 5
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d11fcf1c-b91c-4bc3-a57a-5a3025225f57
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 02486643-da8a-440c-9141-603941da6cfa
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 55ef4063-afc5-4720-b97e-16eebf655ef8
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: b7e404af-a7c2-4592-9563-f4cb50df4bff
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: d2ed4992-a685-495a-9ea4-55e47acb8542
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: b5a2c16a-6578-4a81-930a-52a256d2828a
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 2c26d785-c6e3-49b0-aeba-2f0bdb163df1
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: ecf5c377-d139-4618-89ec-9897f3d3cd48
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 0b2fbe96-4e95-463a-a474-13e2bd858228
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 012c08f9-96af-474f-8ae0-7668505f1df4
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: ac129cab-723b-4e68-a213-23456ec684e7
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 5a6245b6-5bde-4a3b-9fe0-d2be2f74e6ad
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 8cd2e575-0062-4b89-ab07-44d8fb097ed5
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 8ce02c5c-a589-45b3-9f4f-5001acfef2eb
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 862dd4b8-d680-422e-bcb2-890fc5f231bd
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 5c16fb87-d28d-454e-963b-05355b42ee92
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: cf969e23-7814-4a33-a17d-8d166af5c7f8
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: ab0da1e3-2829-4a5d-b916-0e53bbe9e520
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: e0a3e5f0-a31f-4891-b4ec-fa1afb17a444
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 83044011-2fc2-4084-b919-9d990dd69ad4
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 1118e668-c483-4802-acb7-f7ab02e92cb9
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: e4cf4908-8936-4700-87e6-b091a9cbb742
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 40f51a82-f27c-4b57-9958-e7dcac010418
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 4bcb2b0b-0e03-407f-9530-6d2e1218bf90
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 7e018d36-496f-43ac-97f3-6f9b98f913e7
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 3a72ad2c-dbc0-4341-8de1-4ba3de8fd2ca
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: f2eaaaa6-ea73-49ad-aeff-8834123aa195
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: f34f6e22-485e-4a2b-b806-c40b50a651a2
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 7050ad36-1e44-4bc3-9408-8ba813d1d3cd
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 02bcfc37-6f4b-4996-84fa-fd852b85dc56
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: counter <= 11
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4295ab97-304f-4fce-8d62-0c360146386d
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 2bffdb9e-3631-4f40-9092-b8f9e334e097
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: 11LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: be9acdf5-73e1-4fa9-81d0-242da954ed54
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: 11LL * a - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e18ad982-42eb-4e7d-a4a0-45ffb2c50c68
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: ac6d3d73-5eb0-41ab-804e-b1ee1aa352a4
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 4ccfee41-056c-4cde-b062-bb3393f79912
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: fdc89e7f-706c-4fde-ac11-9b7c419c04cc
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 365854e5-e94f-4d58-bd36-ba6aa4f2a379
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: cae7cde5-e22b-432c-a87a-a5b320cb754b
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: counter <= 12
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5da5f304-a91d-444b-a34b-7624b416c880
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: 1224bae7-dc88-4d07-9659-ae2e7a36ba71
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: a939e8e4-ff3d-4209-a968-780764016900
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: d3115796-ffcf-46c7-a002-25c1f5cf7bd9
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    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: be669718-cc35-458e-9eba-747cdf0e4bf9
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9004cd4f-2ab9-4054-b783-71272d6bbd88
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll_unwindbound10.c
      input_file_hashes:
        ../plain/cohendiv-ll_unwindbound10.c: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll_unwindbound10.c
    file_hash: a340dc1e9a375ad2082e9c8cecf3a1a681edcfe0f7220085504fa1991ced3d70
    line: 46
    column: 8
    function: main
  loop_invariant:
    string: r - (long long )y >= 0LL
    type: assertion
    format: C
