- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f3a322ee-7ba8-483f-b805-205573f90e0a
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 24
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3ad255c2-68fa-45d3-a072-f3c2b48e0ea4
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 24
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b30ac8b7-1d1d-423f-9c9d-b5a43630a1ea
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 24
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6fd69e02-ebb8-4a8c-90ea-3195049ca52a
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 24
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )h >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8db62bdb-a429-473b-8620-ec04d8dac532
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 24
    column: 4
    function: main
  location_invariant:
    string: (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9172a093-3edc-40ae-9529-b821c8169a5e
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 24
    column: 4
    function: main
  location_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd17f470-2de6-43dd-8436-3afd50636d67
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 24
    column: 4
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a2bcb62e-f01f-450b-9471-e1061638c074
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 24
    column: 4
    function: main
  location_invariant:
    string: (long long )h >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a751fdce-365c-469f-bd34-a94570a78f72
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c12fffc-4b49-49eb-aa49-7585e3f21d70
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd6689d2-fa2e-4ef2-b262-078b4817e754
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b3d6ce7b-ee48-4db6-a843-fcff9cb12fd2
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )h >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bc301e85-80ee-4f33-b4a0-d9a2ebc81bf5
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14723958-dad3-435f-918d-d5b5a711c400
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 264bf6be-3cb6-4052-8621-8e213945f89a
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e29a9ec-b628-4d34-b06c-350722505a16
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )h >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b8e2c288-a565-4376-8324-e7162b1e13a7
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 27
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a06ca22c-04b5-4f5a-a125-83af945f7304
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 27
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d18ecdf0-203e-4b86-b4f1-cf34b6117460
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 27
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )h >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d04659e9-a895-42d9-810e-7daffd7c3c1a
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 27
    column: 4
    function: main
  location_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 02136d0e-973f-42bc-bb86-2be4048133a9
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 27
    column: 4
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f4014ff3-23d8-42d7-8f19-30bfb44c0177
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 27
    column: 4
    function: main
  location_invariant:
    string: (long long )h >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 18ed6d2d-d10b-402a-9ce9-6166c19840fd
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cad7fd2a-ed90-4455-a4a4-8e05114cbd89
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )h >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8d765c2a-69a1-4047-9dae-133399e1f6b6
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aeab1686-830f-413a-99ca-231048c2a298
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )h >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 704338e4-c995-4f3a-9203-75c6a87b361b
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )h >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d48b2a85-a7b4-4d6a-a648-bfdf444ec05b
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )h >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a3e3a053-f122-4d77-b1f6-8ee07dc1e0c5
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 34
    column: 8
    function: main
  location_invariant:
    string: (long long )n - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 178c02bf-f83b-46c6-99de-608a5aa06d71
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 39
    column: 8
    function: main
  location_invariant:
    string: p <= 2147483646U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 95d0146d-1ff2-4103-9278-1ef8ab906fb3
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 40
    column: 8
    function: main
  location_invariant:
    string: n <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 11caeccd-4256-4327-9c0a-3b39cfa446f1
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 40
    column: 8
    function: main
  location_invariant:
    string: p <= 2147483646U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b9a9152-6710-49b4-9ee3-c5e1b7c1d11f
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 41
    column: 8
    function: main
  location_invariant:
    string: n <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44088ef9-5c36-4da9-aa90-16e109582342
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 41
    column: 8
    function: main
  location_invariant:
    string: p <= 2147483646U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 97332adb-d031-4f9a-8195-b19607db9307
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 41
    column: 8
    function: main
  location_invariant:
    string: h <= 3221225469U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a3c1839-f5a3-4508-a3a7-4fe777427b11
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 42
    column: 8
    function: main
  location_invariant:
    string: n <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 231d832b-5424-4ea3-9be9-1509c0e0a044
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 42
    column: 8
    function: main
  location_invariant:
    string: p <= 2147483646U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: daf6a8f4-9382-4100-a546-cbf4b2b66bea
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 42
    column: 8
    function: main
  location_invariant:
    string: h <= 3221225469U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 107d541e-4246-4dcb-bfaf-cf8d2814ab13
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 43
    column: 8
    function: main
  location_invariant:
    string: n <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f031ba1-f9b0-4268-be53-c5900ed8dccf
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 43
    column: 8
    function: main
  location_invariant:
    string: p <= 2147483646U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 40ce8553-2c66-46a5-98af-9233f0511179
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 43
    column: 8
    function: main
  location_invariant:
    string: h <= 3221225469U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 16d891e7-5b0a-4843-b76d-c2fd52e0632b
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 44
    column: 8
    function: main
  location_invariant:
    string: n <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8cdb0ce7-5fd9-4054-aa5e-5fe1b8ba63b1
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 44
    column: 8
    function: main
  location_invariant:
    string: p <= 2147483646U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2cdf6438-5eb9-46af-b077-48e0fd8cbbd2
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 49
    column: 8
    function: main
  location_invariant:
    string: q != 1U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c9f2520f-da8a-42da-a7d2-5cafb927b66a
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 50
    column: 8
    function: main
  location_invariant:
    string: p <= 2147483646U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a471843-d44c-463b-948f-62ec5aa01616
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 50
    column: 8
    function: main
  location_invariant:
    string: q <= 1073741823U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 450c2c6b-c329-4f6c-b9d3-b59d27d59301
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 51
    column: 8
    function: main
  location_invariant:
    string: p <= 2147483646U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e96ca42-2cb6-4695-8345-20592da3b497
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 51
    column: 8
    function: main
  location_invariant:
    string: h <= 3221225469U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 37225c88-6f8f-4af9-96a5-a441111641a3
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 52
    column: 12
    function: main
  location_invariant:
    string: n <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d2e5f2c-21ab-4c0c-b60e-8947a05c8011
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 52
    column: 12
    function: main
  location_invariant:
    string: p <= 1073741823U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 37d64b71-ec03-4086-812d-5066e1348b89
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 52
    column: 12
    function: main
  location_invariant:
    string: q <= 1073741823U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a391da2-737e-4eec-9e83-df627fb404d4
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 52
    column: 12
    function: main
  location_invariant:
    string: h <= 3221225469U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 30eee638-6836-4fc3-8630-ec4f26960d53
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 53
    column: 12
    function: main
  location_invariant:
    string: p <= 1073741823U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 23dd7e3d-f6a3-4083-918a-1589fedad8de
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 53
    column: 12
    function: main
  location_invariant:
    string: q <= 1073741823U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d776185a-8015-4b3f-bae7-d7eda331f5e3
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 53
    column: 12
    function: main
  location_invariant:
    string: (0LL - (long long )h) + (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1096d27b-08ea-4ff5-84f3-07b6c7b0f00a
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 54
    column: 12
    function: main
  location_invariant:
    string: n <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de589377-aa98-4ca2-b47b-668488f06af7
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 54
    column: 12
    function: main
  location_invariant:
    string: p <= 2147483646U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1956776-fc46-4812-b847-3482abb4e580
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 54
    column: 12
    function: main
  location_invariant:
    string: q <= 1073741823U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d6ab281-1a9d-43cc-92ad-56055e8ff1bd
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 54
    column: 12
    function: main
  location_invariant:
    string: h <= 3221225469U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4275e4b0-4c0e-442f-b79c-48d29b2bc9a1
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 54
    column: 12
    function: main
  location_invariant:
    string: (0LL - (long long )h) + (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 530d0df9-97c3-4971-b18e-9e8987346db5
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 57
    column: 4
    function: main
  location_invariant:
    string: n <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 19ba9271-82d6-4f01-b136-3a6bd53c4451
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 57
    column: 4
    function: main
  location_invariant:
    string: p <= 2147483646U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e44119b-cc11-475a-8b2e-781efb1aa35c
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 57
    column: 4
    function: main
  location_invariant:
    string: h <= 3221225469U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 98e57020-fe9d-4136-bf2d-33666dca94fe
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 58
    column: 4
    function: main
  location_invariant:
    string: n <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 145ea55a-6056-470c-b4a5-b26bac31d43c
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 58
    column: 4
    function: main
  location_invariant:
    string: p <= 2147483646U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c2346289-f5f9-4dd2-9e33-e621407abd7f
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 59
    column: 4
    function: main
  location_invariant:
    string: n <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e0372dbf-15f7-4cf0-ad8b-cb27564f8692
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 59
    column: 4
    function: main
  location_invariant:
    string: p <= 2147483646U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 370e407a-642b-4f29-a4fe-3c97be2ad3cc
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 59
    column: 4
    function: main
  location_invariant:
    string: h <= 3221225469U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3ce75378-4058-4ca9-9f13-46f3d92c087c
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 22
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1c68a28-000e-45e5-93ab-f4508bc2492b
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 22
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d77321b6-aab3-4b8e-befc-9ed140de3c4e
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 22
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 314a4aaf-cc25-4cf2-af83-9854bb1a93f5
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 22
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c5390546-ba03-40d8-be4b-3169610868a7
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 22
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )h >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 92d639bf-da51-4fd9-9a92-a330f957441b
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 22
    column: 4
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6bb2375c-e5f1-4fa1-bb6d-8b1a811081d8
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 22
    column: 4
    function: main
  location_invariant:
    string: (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 17dae63a-27e1-4a3e-99a5-c050582613c8
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 22
    column: 4
    function: main
  location_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2460766e-691b-4693-bade-99c83c1979c0
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 22
    column: 4
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1c86b9ea-5f41-4895-8958-f130dae7f24d
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 22
    column: 4
    function: main
  location_invariant:
    string: (long long )h >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b6036742-9e30-4c81-94b8-40740a5c302e
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 23
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8b8e8ff8-1692-4165-aeee-97cb6cd03075
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 23
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 24e28da5-b245-4f48-9391-e6eff84d5dac
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 23
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c4c8bd2-849a-43cb-8923-80fee59e74a6
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 23
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 47124ac5-2c9c-4353-a5ed-b3e199b45032
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 23
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )h >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3cfa557a-40bd-40b1-96ab-72f5b9f9a781
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 23
    column: 4
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a247d6e-deb8-4d16-b631-d4bcb198d225
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 23
    column: 4
    function: main
  location_invariant:
    string: (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aee006ce-7381-4cb4-ad84-1d826fa86545
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 23
    column: 4
    function: main
  location_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 444f8063-096f-42d7-a957-06a2e90cf5c0
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 23
    column: 4
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 840c9bc1-b5a6-4560-9e63-349d60997da6
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 23
    column: 4
    function: main
  location_invariant:
    string: (long long )h >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 782c6c2d-728b-4f56-ad85-8d73c79bc2e7
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: n <= 4294967294U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0936a788-9886-4605-b4f9-fd2fb6ce22e8
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: p <= 2147483646U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c10b35a-3b0f-4de0-9ccc-50db9da4df26
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound100.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound100.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound100.c: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound100.c
    file_hash: 5bba06987e8c2f8236800dde4bec4c9d50f427f841de99efa853660259681b37
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: h <= 3221225469U
    type: assertion
    format: C
