- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d6a970e-09c6-4132-a605-4eddfa881dc3
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: d3c31d38-3ce0-4794-a4e6-ca06640bd7ee
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 1889413c-acf8-4fc0-8cca-7274c12a2417
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 6a891c30-30ba-4c78-8f40-56275a91400c
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: c4420746-d559-4b6e-80ba-7be43fb55877
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: ebe88fff-532d-42a2-a5e6-dd5b76315c16
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: b6eade0d-5055-4232-87f1-d2e6e8995d6b
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: cd162dc2-c684-48cf-9f61-90cbaffb3ee4
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 9db91e4a-115e-42fe-bc4a-ac06ce360480
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 3db433e4-c5a9-4e09-941c-5b2e2efe13d3
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: ded21d0e-650d-47db-b6d5-743e4aca713c
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: cee1ad01-f255-4c20-a859-7b76e1665b39
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 2cda11f1-26bf-4e93-b736-204755debed7
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 5ff43600-c325-4388-a491-f74623bbf1c6
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: b86d99d3-e9d8-49c9-b151-b42ea53d4fda
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: ddc29e88-898d-4f52-8f80-25f05b107aa5
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 01bc85dc-264b-4cbe-9c4b-eb274ca69760
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 16278ed2-3103-4132-84e3-28154215b84c
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 275019fa-a096-4ab1-8e88-4f5be61b7639
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 4191fcba-0595-45e0-9f0d-d2925f2e53a3
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 187bd79b-3343-41d6-9e05-34eb7fb22e78
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 2aad7ef2-27ac-4448-865f-0282caef5398
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 3b87c220-aedb-4d10-b480-c6282d527585
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: bc3ad0fc-4d4d-4a5a-a868-23833807d119
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: fe409338-133f-4194-8f32-8e05ac0a52ad
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 2fa7f418-7bd5-4c8b-8757-4918b30feb39
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 2e66f1a7-0465-40f0-a0b3-68d461446525
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 4734b904-d4c9-42a2-a173-977daba8062b
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 66bf4d05-b9c5-4050-b291-0422c2dbcc79
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: a5d5abab-db66-44b2-88d6-9c9e4e3f0172
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 11abefae-4628-4127-b121-112192bc544f
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 6a2897c2-da37-44f1-ab80-0979d7fb3f2b
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 1ce70d1e-8e9d-4bf2-9663-67877e5827fa
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 99ac897d-e294-420e-b754-90c5a0e9fa30
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: a6657e47-0d9b-4653-b821-e9eac90bfddb
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: b7ba41d5-e8ea-4f3e-b30e-f5d182a7f5fb
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 2719572f-26c5-4436-889e-7145d4201fcc
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 81b54e19-2dfc-4ba2-848e-a0bae24dd9fc
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 845ffc21-bbd7-43d0-ad01-355a0f1096a9
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 87b951a6-654f-4cc6-a473-9931166c901a
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: b406e75f-41e5-41fd-8fe3-37e06f28ea3b
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 1787be65-016a-4b14-800a-fc65a0b113d2
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 642496f7-f38e-4913-8fa7-cea7756d75ff
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 2bb3599c-43ec-4f12-b291-63230df9f4dc
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 65a94ce8-4191-4636-9b0f-68aea21e3e40
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 360f85cb-c6ec-4df5-b586-38be3da522f2
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 3ad5d986-efd1-4a86-a54f-dacc66dfcd6b
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 1755c554-ad83-4597-839f-db6fde1c686c
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: ae875378-5192-4897-be82-2fbb891c7e72
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 0a5f605b-6e31-4d62-ad45-216da073a9b6
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 7896a31d-0f9c-45bc-bbb5-2a6225d441bd
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: e746327d-506a-4fc5-9daa-24e4f660b779
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 3179f9b2-d643-4c9a-8bf9-cdebef8bd238
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 4790bd02-4954-4568-a554-52411549eadd
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 8f1f5731-cb3f-4e83-8ae2-f5c28f289f66
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: df1b7ded-a0f1-4696-987d-991ee83f8ee0
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: c9c58445-5d90-450c-ba96-d476f3cf8a17
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 7b92906a-3604-4411-85a0-448e1104a962
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: c1ced88f-267d-4a48-8076-1f0ad8ea5f5c
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 73c037bb-e14f-458a-b3cb-8309de6ea387
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: f43ce1d4-8d88-40a5-8b10-61fa82697346
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 0afd11fe-2a19-478e-9256-1cffa26d72a5
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 8927f13b-16ef-4d10-9208-b5fa8c35166d
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: bd900827-69d4-4809-8f30-d20990d0564a
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: eaf245d9-172d-4009-bf7b-cf968b68f1b5
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: e57be0b1-8b77-4241-b0c4-454f5bac9e44
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 82a3f6da-ddd2-416e-a90b-22bcf8a09163
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 390cad69-5aa2-420f-81c1-ed054aec9eba
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: df3787f1-5df5-4f4e-83b6-33aa19b9b5ef
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: ea3bbc3f-b785-4a6f-a8df-f31708bd58ec
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: cf0a2093-d495-466c-93e3-b00d593e3e13
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: eaf24cc1-0969-4551-bd9c-d82647afc2a1
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: b241ef7f-ce0f-4f61-8334-ef56ae8f289e
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 2d8b195e-229c-4c82-8562-570c4e2314b7
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 434b8512-a15b-43ff-bf8d-c76d46040364
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: a7e203b3-53e9-4d55-8a32-55086b5cfabd
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 57683a77-9697-45ec-8698-dbba3e5d969d
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: c7b6d8ac-d01f-413b-ae15-8b039579aeaa
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: f8ad8122-9c91-4f8e-a08f-fd707edbe968
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: f2d51e13-e90e-4ead-9fd8-cf397c10b83d
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: f8f28b7d-020b-458d-bc80-4f1a9684cc32
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: d96ec13f-b799-4b18-9137-9a558b932c7e
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: efb0751a-72a3-48c6-a332-701de08a7de0
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 3adf0a37-85e8-4b0c-b505-0f95c31a2833
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: d035f148-d01d-4ea2-a4fe-e892dd208035
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 2fb4910d-777a-49f3-8d76-d6221fd447e0
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 6d20e5a5-4675-44cd-9f34-6098ebabff53
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 229b983e-0559-432e-8250-75c975f7e828
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: ed3417a3-8195-4e46-b787-2ed4c7e9db8a
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 658eb367-7b9c-46d5-8c14-e68883ea852c
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    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: 190930e4-1e00-4eea-9da8-eddb7af94c1b
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound2.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound2.c: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound2.c
    file_hash: 185af411ffb66b9762afca1cabf119211700e2cdb0b48054cece4906f7290e44
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: h <= 3221225469U
    type: assertion
    format: C
