- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0d895448-49e9-41c0-959c-1322fee9b71c
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 37
    column: 1
    function: main
  location_invariant:
    string: 0LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 62647dbb-0992-45d7-995d-cd3190ae7e54
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 37
    column: 1
    function: main
  location_invariant:
    string: a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 216b843d-de2c-429d-8f60-2e9a3685ea11
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 37
    column: 1
    function: main
  location_invariant:
    string: b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d64586e0-967f-4ff1-b66a-13bbaddf674d
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 37
    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: ed70be46-1aa4-429a-b71e-ec23ad75218c
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 37
    column: 1
    function: main
  location_invariant:
    string: ((0LL - b) - r) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb35cc73-b0e3-429a-b2fc-2e43d48dcfd7
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 38
    column: 1
    function: main
  location_invariant:
    string: -9223372036854775806LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 740374cb-467d-4955-be3e-3dd61a6197f8
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 38
    column: 1
    function: main
  location_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e86fa73c-acc5-4107-a390-d2a4a574ee5b
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 38
    column: 1
    function: main
  location_invariant:
    string: r <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c89c16ee-15e8-45ba-a0ee-409b1969af8d
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    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: 10330621-ef1a-4cde-8936-a0f122443a06
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 38
    column: 1
    function: main
  location_invariant:
    string: b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d6f94e10-22e9-4d68-8c94-b533862e5bd6
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    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: 2515574b-7fb5-4d3d-974d-f7c0fa18f9f0
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 38
    column: 1
    function: main
  location_invariant:
    string: ((0LL - b) - r) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c3cd11d-0d06-4da6-b3a4-4a83ceeb476f
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 40
    column: 5
    function: main
  location_invariant:
    string: -9223372036854775806LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cb638a1c-4ed4-4ed6-800c-f48ec6579ab7
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 40
    column: 5
    function: main
  location_invariant:
    string: r <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c6a1bab7-3396-4bd8-8b80-fb629c200a67
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 40
    column: 5
    function: main
  location_invariant:
    string: a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 97fea95f-4daa-4ca2-940d-070ce41524af
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 40
    column: 5
    function: main
  location_invariant:
    string: b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 203cb948-aa32-4493-a01e-18b76843045e
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 40
    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: dad987ec-5bd4-4095-abbd-f20668585af3
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 40
    column: 5
    function: main
  location_invariant:
    string: ((0LL - b) - r) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e760a070-e896-4d33-a09d-d8574abf732a
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 42
    column: 1
    function: main
  location_invariant:
    string: a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0d0c19af-7972-4ac6-bf3c-1571265d3754
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 42
    column: 1
    function: main
  location_invariant:
    string: b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9fea5af5-90d5-4491-856a-36bda33f88a2
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 42
    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: e060559d-2093-46cd-89e1-5fe0933553ba
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 42
    column: 1
    function: main
  location_invariant:
    string: ((0LL - b) - r) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 62c49d7d-bb6e-437e-9cf7-29711931ab59
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 42
    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: 559a53dd-e68d-4dab-8400-1f328cde4fd7
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 43
    column: 1
    function: main
  location_invariant:
    string: q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2357a9fa-ae74-4746-aef5-8ab46330df01
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 43
    column: 1
    function: main
  location_invariant:
    string: b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3dccdab7-3faf-448c-a6fa-6d27d935748d
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 43
    column: 1
    function: main
  location_invariant:
    string: ((0LL - b) - r) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d252ede0-3705-4b9d-889e-dcaf4e4cdf52
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    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: c2dec62a-0b88-4820-a63f-ab714aa3e8f1
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 46
    column: 5
    function: main
  location_invariant:
    string: 1LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2594b146-2072-45fd-8f78-618b5f82c20c
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 46
    column: 5
    function: main
  location_invariant:
    string: q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9ebadcbb-82ea-4100-ae84-66034bdea0b6
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 46
    column: 5
    function: main
  location_invariant:
    string: -1LL + a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 60e373c5-d01b-45d3-86eb-89b61be8d5b7
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 46
    column: 5
    function: main
  location_invariant:
    string: (0LL - r) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 77ec6e2c-5db0-474a-b9aa-e5339eadaf7b
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 46
    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: 5eeeb870-7380-4ba9-9419-659432120c09
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 46
    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: 3f17242e-9a35-4a9a-b402-b29f58dc1ba4
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 47
    column: 5
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 478c0b00-7b3f-4bef-9920-91230540e136
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 47
    column: 5
    function: main
  location_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f063f997-6951-420c-b078-75abe796e14c
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 47
    column: 5
    function: main
  location_invariant:
    string: r <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d482d90d-2323-4164-9bcb-89f7c4bf34a9
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    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: a50a615c-2474-4cc5-90fb-8c05f93111f1
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    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: 885a0a84-f940-42a3-b2b2-2b0f64087f24
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 47
    column: 5
    function: main
  location_invariant:
    string: (0LL - r) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3f9d278b-3796-4c28-a913-972c62347a65
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    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: a65ebc02-0ff6-4d17-a9ff-a5016c6fd4bb
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    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: 571a51cf-3415-4267-b855-dbba935d6b9f
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    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: 60396103-e089-4e63-9bcd-08a26937a340
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 48
    column: 5
    function: main
  location_invariant:
    string: r <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e97041a-7ee1-4bff-b03d-d94d2e9f1402
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    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: 4d0858ab-f43f-4804-b6fc-f2410b081208
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    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: c8b0d55c-1867-4f6e-b658-276718d71f99
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 48
    column: 5
    function: main
  location_invariant:
    string: (0LL - r) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 70c92534-c80d-4f16-8e87-6bd4e63cf4b8
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    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: a33e1874-3d74-4338-9d00-9f581a9bf13c
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    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: 28aa6bb2-5dd5-43d0-8fdb-1677c63ac05a
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 50
    column: 9
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a9b0d03-9145-42d4-ae30-0d0ca2e1ad52
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 50
    column: 9
    function: main
  location_invariant:
    string: r <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 399fcfd2-3fee-41e7-8107-d7435e27a170
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 50
    column: 9
    function: main
  location_invariant:
    string: q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ba66a4d4-bfcb-495f-9917-0d8dc49641d4
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 50
    column: 9
    function: main
  location_invariant:
    string: -1LL + a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7db3623e-fe3a-44af-871d-e9c01ac93b86
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 50
    column: 9
    function: main
  location_invariant:
    string: (0LL - r) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ff2c2bf-1ea2-42e2-8e0a-7df169d6015b
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 50
    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: 57d4ad2f-284d-4599-849b-ae190ab677c8
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 50
    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: 1f63c3e1-8f4d-4a22-a98d-382f3c1514aa
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 53
    column: 5
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 72033f84-b736-4d47-b898-155d20ae5cf7
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 53
    column: 5
    function: main
  location_invariant:
    string: 1LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 123a5aed-2eb2-41e5-8846-373efe49727d
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 53
    column: 5
    function: main
  location_invariant:
    string: r <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ea122eea-f0d6-4274-a1fe-d9093884a257
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 53
    column: 5
    function: main
  location_invariant:
    string: q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6730b32a-5098-4d96-a1fa-b84ad1b7bbc4
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 53
    column: 5
    function: main
  location_invariant:
    string: -1LL + a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 34f6ab71-65f3-49f2-b358-5aaf3d90c25c
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 53
    column: 5
    function: main
  location_invariant:
    string: (0LL - r) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ae67b2f1-a2b1-4cc8-ac97-246eeb5fe3ac
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 53
    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: c7106e3a-c30a-4ed7-a6ce-43db5cac9ef4
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 53
    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: ceaa9b4e-3895-4099-a94c-9bbc61006184
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 53
    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: d56fbba0-31d0-46cf-a1fb-536f68b01693
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 55
    column: 5
    function: main
  location_invariant:
    string: 1LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fe2b2094-5800-4fc5-b2eb-46a8046fae99
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 55
    column: 5
    function: main
  location_invariant:
    string: q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd270528-86f9-45a7-b3f2-2b30956fb0e7
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 55
    column: 5
    function: main
  location_invariant:
    string: -1LL + a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 22605e30-1fe9-424c-b43b-c717b8d2b7e2
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 55
    column: 5
    function: main
  location_invariant:
    string: (0LL - r) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e7e6a3c4-3f20-4f1b-a60a-42fdcc8d53da
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 55
    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: 7e07f2b1-9b72-4db2-9236-6fa8841f65b9
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 55
    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: dcb44411-c053-4c26-882c-891bcd0b1d2d
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 55
    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: 3789ce73-9113-497f-b2b1-5a7829d77a61
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 56
    column: 5
    function: main
  location_invariant:
    string: 2LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5a014dac-cab6-4106-821e-1e14de8b1542
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    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: 89f8c757-2369-42f4-b9ed-2c1a9873a3ac
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 56
    column: 5
    function: main
  location_invariant:
    string: -2LL + a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 828d343d-1f39-4a51-888c-bbbb6b426e51
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 56
    column: 5
    function: main
  location_invariant:
    string: (0LL - r) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 154a6031-39c2-4f90-be97-c6269f1fad17
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    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: 4ee59267-0d45-49ed-8eab-9ada30f8cf66
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    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: cc54f759-0fc8-4831-ac84-3fba46ca1a11
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    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: 9ac1ec93-2036-4d02-9606-7e25d6f0c2c0
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 58
    column: 1
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 10295d54-38e8-405f-882d-abeababa6672
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 58
    column: 1
    function: main
  location_invariant:
    string: r <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 05b48841-29a7-4af8-bc55-a80411db1d25
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 58
    column: 1
    function: main
  location_invariant:
    string: q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3f066434-0ab4-4a53-a865-4b9c64d233cc
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 58
    column: 1
    function: main
  location_invariant:
    string: -1LL + a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eba010bd-76a6-47cd-8bbe-9f5ad5715092
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 58
    column: 1
    function: main
  location_invariant:
    string: (0LL - r) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1668f388-1fae-4760-aa2d-e63a62cbbe88
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 58
    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: b309f9e0-e455-407b-860e-63179ef1de82
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 58
    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: 5e4e5938-4896-47a9-89c4-a31399ed5f0c
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 58
    column: 1
    function: main
  location_invariant:
    string: (-1LL + 2LL * b) - r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 68bc7843-ed4a-4ed0-99c0-6d1af5c7a628
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 59
    column: 1
    function: main
  location_invariant:
    string: -9223372036854775806LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e0a48aa-13a9-4a1e-99b6-4e2d96437acb
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 59
    column: 1
    function: main
  location_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 01210938-b0d8-49e4-a3fa-e58b056a6ce6
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 59
    column: 1
    function: main
  location_invariant:
    string: 1LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e45373ab-8829-4a91-be25-2c8c03d70e23
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 59
    column: 1
    function: main
  location_invariant:
    string: r <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dcb1e007-42e1-423b-8912-0168c91d8010
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    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: f03610aa-7700-451e-849e-3ec4d57e1ebe
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 59
    column: 1
    function: main
  location_invariant:
    string: r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 96123e99-c62c-488a-b652-965a254040c1
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    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: 99c92d14-81ee-4372-b6d2-48658bc08a28
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 59
    column: 1
    function: main
  location_invariant:
    string: ((0LL - b) - r) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 92336c9c-40b7-47ad-84dd-be0d5db1338e
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 59
    column: 1
    function: main
  location_invariant:
    string: (-1LL + b) - r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 17f09bc4-38c9-4923-b097-8c9ec31d6686
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 59
    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: 59714917-fa76-41b4-bc06-853babeec4d5
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 62
    column: 4
    function: main
  location_invariant:
    string: -9223372036854775806LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eecc8234-245b-4586-9e38-6e3693066dfe
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 62
    column: 4
    function: main
  location_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 96c8ea55-26e7-42ab-b17c-7bc2e8d9d7f0
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 62
    column: 4
    function: main
  location_invariant:
    string: r <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 59e2e2cd-7906-4909-877c-d4f3d7b2ce71
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 62
    column: 4
    function: main
  location_invariant:
    string: a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 827c3d50-bc95-462a-9566-e33fe1951480
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 62
    column: 4
    function: main
  location_invariant:
    string: b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0b40ce35-327d-4f03-824b-ca8660aa28d4
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 62
    column: 4
    function: main
  location_invariant:
    string: (-1LL - r) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 51bd6e01-e949-4333-9598-b574dc034f69
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 62
    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: 5ee83583-93af-4ac5-bb76-f1df5dae8d54
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 62
    column: 4
    function: main
  location_invariant:
    string: ((0LL - b) - r) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0bc8c99b-49d9-44be-b9f8-2f17083c4a11
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    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: 5b2425f0-229a-477c-ad57-c511d9852666
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 63
    column: 4
    function: main
  location_invariant:
    string: b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d761ff5a-b506-498b-8753-22ae2901a467
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 63
    column: 4
    function: main
  location_invariant:
    string: (-1LL - r) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5af1ea2a-3a45-4cdf-ac38-022ff6b85036
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    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: 27a1aa87-e1c9-428a-a121-b8662bbcf2da
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 63
    column: 4
    function: main
  location_invariant:
    string: ((0LL - b) - r) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e5317cb2-0e1d-4836-ac10-2b975fcbbc4e
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 33
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e336c3e4-41d0-4fa5-acc5-adb4d0e2d879
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 33
    column: 4
    function: main
  location_invariant:
    string: r <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e78de1b6-e0ba-4810-8d89-7dba385b2c59
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: -9223372036854775806LL <= r
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 34a66ef9-937c-4a5c-bb00-d110b4ccdafd
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f324635a-da34-4063-b1d2-fa5615067c5f
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 941ed8c5-345a-465f-be58-bb577f66f77f
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: r <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 02a3696e-7b55-4a54-b107-4d4b1867f070
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: a >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 16738cce-595d-414e-8d99-95bd9e33d736
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: b >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b2db9e2d-43e8-4e3e-9f34-ddbbb27e5aa0
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 36
    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: 804a1258-e0b3-42c2-b6cc-7e92f68951ea
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: ((0LL - b) - r) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c9fd379-062d-49f4-81fb-ecccfdb63af0
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 45
    column: 8
    function: main
  loop_invariant:
    string: (-0x7FFFFFFF-1) <= r
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6391c642-2df5-40e5-9244-85f8b786f8cd
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 45
    column: 8
    function: main
  loop_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e6b65fed-e439-4421-9741-0309d82f1492
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 45
    column: 8
    function: main
  loop_invariant:
    string: 1LL <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e5fe50d0-5347-45e4-9ee2-daf0d1f0f1f7
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 45
    column: 8
    function: main
  loop_invariant:
    string: r <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 16ddf1ae-6f1b-496e-9a43-b954e8a98eb0
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 45
    column: 8
    function: main
  loop_invariant:
    string: q >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ac5b2ca-2447-4ed3-a4b2-ae11e284f955
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 45
    column: 8
    function: main
  loop_invariant:
    string: -1LL + a >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e90847e2-d32d-45b9-875e-e8487b53c77d
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 45
    column: 8
    function: main
  loop_invariant:
    string: (0LL - r) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a930fde-0c1c-478e-8234-42385dece928
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 45
    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: 00415aac-10bd-4435-917e-cfc3df36d90e
    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.c'''
    task:
      input_files:
      - ../plain/cohendiv-ll.c
      input_file_hashes:
        ../plain/cohendiv-ll.c: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohendiv-ll.c
    file_hash: 601ddeb38cc85433f6271611bfd2617c2fcbf2b89119dbe2c319aedc14aa3b17
    line: 45
    column: 8
    function: main
  loop_invariant:
    string: r - (long long )y >= 0LL
    type: assertion
    format: C
