- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 364ca047-95a5-43d2-a70f-084d4a3a502b
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: c413ad61-b0fa-4ff2-b697-4ad3f494bcea
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 6d0beedc-e65f-4377-9d83-9fa329527659
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 9a97e322-b677-47a6-800c-6d408c209bce
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 510ddda9-bc53-4087-9b71-1915cf3e7654
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 777a500d-d7e4-47ca-97eb-a03ecf3dd93a
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 78e3d3cf-374a-48d0-8732-c2111630b6a1
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: e1972a4a-d833-4fdf-a430-be359651bc03
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: b0e45b6a-880c-4942-b8dd-79c81745fd27
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 43d0368b-8a94-4edb-98e5-5bf295a6575b
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 3a31d2ef-a42a-484b-8b54-e00ea7944776
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: aca0d1c5-0ff6-47ce-bee6-ec1836db8afa
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: a74e64ee-93ce-4ab8-aecf-949e2757bf00
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 16adb5a6-7e8a-44c3-bc5b-d38d5a10abef
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 4f9b6fd9-9ad3-4f10-9995-799e699a61e6
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 3e35e1fc-8c8a-4915-89fc-adeab49a55ea
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: bcd50440-08b7-47b0-8f90-cb75231edbe1
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: bc59e67f-d81b-4498-bf42-b8d8fc1cd0d7
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 7392a5ec-2698-4cbb-afc4-8cf265e65d2b
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 63e55d7c-35c2-4104-bd5c-048973187f82
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 0ac05beb-2504-49b0-9880-2f0b2b20e8c4
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 8e177931-da0b-494a-a5e1-6a20a342382b
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 0e8ba99a-e5fa-4711-86ef-a3c6c6a6101e
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 9430b0a7-edb4-482e-92a8-b0376a0f8afd
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: da845817-1130-48c9-9982-6b4d1f9dad55
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 9fc65229-8031-4398-abca-3b8ac59efa59
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: bdb7f5fa-4ce6-43fc-9221-b29c35ca5615
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 949a53d1-1f30-49e8-886a-d7b90489e184
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: e284937b-63c5-4d21-9728-b3d3ebc0939e
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 7ab03e76-5748-4e53-a8b2-41220e978f95
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: ece27c4e-ba1a-4531-b56d-344df683bda1
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: b415678e-ec56-4ee5-9b00-61b5f55b888a
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 807138ea-9101-4852-992e-5126c5f4d360
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 70a0a125-804e-45e3-9f0e-d4b8317ed422
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 6db53e9d-7248-46a2-a00b-765792c255e9
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 5623a285-c16e-433b-a7da-b3add1dedc63
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 1c5c4514-63ae-46db-b084-56ce32d33450
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 6f59a797-624d-4d83-810e-0973362bf70a
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 1a25415d-9168-46d6-a0fc-d80633da0b4a
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: b7e50aed-0367-414f-bda8-01b1fa943fd0
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 53d360de-0c87-49e4-ae24-8ad4190de027
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 3acc5ca2-ddbc-40b0-b82e-a38fd0376873
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 8c7909b5-489c-41fc-b263-0f997ab253bd
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: bac17b55-eba8-43f5-9690-9eb8d3fd4497
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 70abf551-a58f-4e49-86a0-3c792e57d355
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 7bffc155-5853-489f-810f-dda93ac401e4
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 9af369d7-94cf-4006-b1e7-3a8af668af7d
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: e583fa59-2f0b-4665-9162-138f6176b220
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: e2cc3715-dc56-4638-a257-a56f9a3a9085
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 61e20108-53e4-421b-a4e8-8114c478cb1d
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 027dad6d-af5c-46a2-8b4d-91059bd1a9fe
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 20295d55-0c49-4648-867d-dd7329ea9d62
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 36b0d14c-d126-4b83-b9c3-7288b772036a
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 2ff7b88a-cc96-4d3e-a893-1affdcc5db1e
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 56e2f636-b8e0-4213-ac6d-f5e42aa3b531
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 0a31fcb7-8791-4752-a9f3-208d16d9d519
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 381d435b-d500-4f0c-b8bf-39448855177f
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 30f288f7-bd2c-4473-a7f3-83d073461aa7
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 85e67378-dfdc-4cb9-ac33-3a0425e93fd8
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: e836314d-d30f-40b3-a023-3cb42d559362
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 5001396f-35db-493f-b7a0-6224316eaa48
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: beae8a80-e058-445e-83d5-22678ef23f15
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 0643d286-298c-4da6-b552-de7ee823e1ea
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 4c2f1871-c3af-4b96-9d81-9f01abf6e7dd
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 559e5219-b30a-4aa2-a472-f7ac1000d943
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 94bae427-ef11-4b52-ad40-05944edf625f
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 9793c8fc-88ca-4cb5-9228-fccfb63bf14a
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: e565670a-848b-4c90-8c9f-92b35d787a0d
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 670781eb-00ff-47e6-a51c-107cc624918f
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 6cd142b2-0ef5-4c20-b7f7-e9a4a6883583
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: db1471a2-7162-4dbc-bad6-465ba04c2f73
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 2b45590f-f0bf-474b-828f-749171734d97
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 1a0ebd21-7421-445b-bf5e-ed17b7eef6cb
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 008eb57d-8ff3-4ac6-b2d6-69f387b6a348
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: be3c51db-ca30-4e83-9582-9efec70679a4
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: dc2d1080-844d-4a62-b181-ecce07ea64ea
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: cf3dc9fd-0383-48e6-aab1-673d2526c5ff
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: b706950d-ce23-44cb-9a18-bc2146b073bc
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 40fd6a2e-9248-4bb7-a013-b4fbbb6587c4
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 6cd3b4f0-8eb4-4371-90ac-03439d8e8917
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 0f1a8a72-4b46-4116-a6c2-1a4029272e4b
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 46b9d598-9f72-4921-945b-94a621390a7b
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 942f02db-2d89-4047-ba93-f76923db81bc
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: da0d3ce2-7ab6-4a51-b42c-11e4cfaa0512
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 904a0ca8-8c5e-4a0d-8d69-b2a79b6aa104
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 33017938-9ee5-4579-8911-5363740aa541
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 6345849c-9ed7-44ec-a3cc-32e6c904b613
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 0989b427-bd58-4d8b-b351-da4f80ba7321
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: ae814bab-fd25-41a1-8b46-4582d9a7dedf
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: e0b994fd-9f84-4a89-9b8e-6a39e8768294
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    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: 74e59879-d9c0-4b21-ba39-6266064129b3
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound1.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound1.c: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound1.c
    file_hash: a2e0d3ed79ba62190a0b501c090bc81fd178363cb7e6ce8cbe0996ce655e2ac6
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: h <= 3221225469U
    type: assertion
    format: C
