- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ae4f9368-2b97-4e6b-934c-20257bce761b
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 80df7904-af32-4523-9c4c-06335304b5d5
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 13a49e80-2c61-45d8-8cbc-6afe03e6ece5
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 81806ca9-defb-4f1d-9123-1ad6176009dd
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 664cde94-a8a4-4d56-ad71-382f4f0c6a63
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: b479fc03-4d3c-4b3a-85f0-ae60f10859c9
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 275ee248-81bf-4244-a34c-92822eff7935
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 15d70d98-5445-4e17-88f9-0c141c1586f3
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: cada31e8-cec7-4be5-85d1-3acf5bd307f1
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: edc6f61a-c753-410f-9505-e109e1177fbf
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 2e67e32f-1bc0-4e54-9cc6-f7e29dedb2f8
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 0db3c32b-a593-4565-8e99-5c646b7dd70c
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: e4a8373d-0d15-4575-9ecd-c5819f963a04
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 85d9cd9f-036f-4576-aa11-b00ffdf2fb01
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 0674d680-b92d-46fd-9cf1-e1b5e99ae138
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 7e3d1f6f-6f9b-4f5a-ae38-8c3f54ed7c44
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 3639d04c-b41f-4767-940b-6fb9b7002a67
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: da569756-3483-4f80-a9f1-25e5c75bd9a0
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: dce3847b-fd7c-4950-8d06-2278e9da0493
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 0bdf1f72-a895-4386-bad5-a9396d832aee
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: f0c84520-3b2a-4085-8cbe-0e0ad3f92ba9
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 14a02ba6-58df-4bc9-bc35-9355d679f94c
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 87f70b5f-de63-40ae-854d-7cdd76ec8ac4
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 2310e319-64ac-46d0-ae01-491e91bc1acc
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 677a7a61-e7f3-42de-840e-2d55031571eb
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 0507d7a6-984d-4c65-809a-7743bf441fa6
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 9a2b5350-38e1-466d-be73-b6ba12fc6b17
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 66e23e6b-544b-4213-8064-4e76ed93763d
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: bba339d8-2b8f-47f3-89cf-899a15d8a317
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 54a8fc9a-0d60-4b6f-836a-ce4eeb231f24
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 1aab69ca-2210-4afc-9dbc-9d167cb082f1
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 5cb46f2d-4201-4a29-9857-5c7d6d717c68
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 3046f74d-8432-4827-936e-74b24930a45f
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: ee0e4eb5-c0a2-4017-87a2-c7d4da3a06b2
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: a14d08bd-07e6-4e9f-852d-d8fd60469de1
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 0f9213c4-8ff0-4576-af1c-8db36de3c6d6
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 282b94ba-43b7-452f-babd-87417ce22c22
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 0e1d9cb7-ec50-419f-a8b5-b7d36958f884
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: e24af29a-9a42-4060-98e8-808b5b081c87
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 5b03d8c1-3add-40ac-aa90-2cadb79f93f2
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 4b5a0830-5b68-452b-9272-b4ef18fc0385
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: bb8c8be6-b423-49b6-a34c-8e8b983d4e5f
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 1f8bbd60-6d95-47df-ae9a-139d2af9a5e4
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 6a68734f-a1ce-46e5-b45a-c541ffe77ac9
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: f2930187-0b95-42ae-a83c-0a29c3bb960d
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: c0d45d15-0bbe-4e5e-8668-b590f1724899
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 9b84e711-eaf8-4291-a477-f5cbdf97b0ef
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 31b0976b-d042-4b18-8372-ab0bc970acba
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 4f7cc8c6-770e-4beb-a022-4dae046c98af
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 9f2f88f4-02b6-48bb-8f89-4f7cb6cd5186
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: ceccceb3-cede-4140-bc9c-c16bf4a9b3b5
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: eb671cea-2fc6-4737-817d-724d81b1a076
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: f9254d7d-390b-4bb8-a636-872110330d3f
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: c37a07ac-1d2d-4b33-996b-56a59ca4b3ad
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 22232da3-1d97-4ec5-afd2-d330223528ce
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 8243ae2d-3b1d-40ae-803f-c0db4c0b1bc4
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 225b9bd0-d78c-4f10-b837-94de8d34c98d
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 4e3a77fb-5115-426d-bca7-bb0e5d0a0571
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: c8260e77-f68f-4d96-8eab-b6c5fff7c5ca
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 61bb8c9e-f215-46a7-8b40-7af06fc2314c
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 4cdd8e1a-26e3-425f-bda7-e62f89a171a8
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 069b312d-128d-4b8b-9cd7-de1d346a8c02
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 072cfe03-8b61-4b07-9055-ff59b8457f04
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: c1b3b8c6-7382-42a6-b888-9c9cb7ee129c
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: dbeb0281-443b-41b6-8661-e64d485b6cad
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: eced1915-d923-4970-95c5-e9cb62af2c3e
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: bf8fff89-18ac-46c8-a365-a329f4f1334d
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 94030edd-72be-4839-8449-215d6513f0c1
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: d93c12f9-7d13-4076-9832-1d1ab2096229
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 522bb922-aa48-4557-a11f-398288946f82
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 76575b68-de18-4b23-ac85-b5a6d1a88494
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: c38a8df7-13fd-4a56-b780-0a914e8b3f0b
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 2ed956e7-a18c-420e-b3f0-8ae1990dc8f6
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 347981a2-8e6f-49ec-a9c7-bd920167cf69
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: ca758ea8-b094-41b3-9806-b006ea0b2e4e
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 3b1544e3-6ff4-42d7-ac0b-2fab6794e435
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 5f70f57f-307f-41e2-81a3-02f4e764de0f
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 3024ac45-a339-4ad0-be79-a07c74fccf9b
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: d20e30ff-4b15-4b22-b6eb-ad54559ed05b
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 96339f1d-f794-491c-81c1-8c087ac7012b
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 299577fa-1fd7-4bef-a2cf-cd478f44726c
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: a8a533b8-f35c-4b18-9ff5-a97cddd72ffc
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: aec02059-84f2-49cc-88b0-896af28d14f3
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 15e9242e-c638-4a5c-9d93-c4c713ae476b
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: ef149088-9d9f-46f7-b413-d3b2ec141bbf
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: a1d1713e-e433-48dc-a2fd-443aab982ac8
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 2c40ec23-056c-46bb-882b-0690376227c5
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: b2dcdc1f-d6b2-439a-8c97-5ffcdc0e42ed
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: 5220edfe-635a-4728-98fe-92432586328e
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: e801b70f-353a-4e67-90b1-e69ce8628c6f
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    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: d49e2808-0c25-41a4-b85e-2c098e9ac317
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound10.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound10.c: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound10.c
    file_hash: 74bed2c5921e53f16e234cbc0a2deaaf4b0b51c6cc3f20bfab2fd33a0fce7ecf
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: h <= 3221225469U
    type: assertion
    format: C
