- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 21adc014-6bf7-464b-90f3-2fb2c8815f07
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: d6c17e02-9a3c-4ddf-82e7-a6613d53a63f
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: f295bedc-8c59-4a9d-be57-baeb86fffb61
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 5a7c6dc5-982c-42ec-b7f7-0fcb7b5acab1
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 37d33cab-f3f8-49b0-aa11-3ada5de0f8c2
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 2888789e-23d4-4133-81e7-2762223f30f9
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 2e4da678-ee7e-42f7-ad0d-d63fa001b878
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 7fafe0c8-44cd-4a12-b988-f3d68e1e48f8
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 915d40e8-0e38-4ada-88f8-5bf0f2889dad
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 27d902df-ea65-42b3-9060-1a399c942972
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 900486a3-6423-4425-86dd-d1a712d5cb03
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 20708737-f36f-41e1-b216-04dbafa9bf29
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 08bb4a42-e7e2-4156-b5d6-25694b29f8df
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: a20ed350-3c3a-424a-899c-87f70ef3c9f0
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 9574fc55-f66c-43df-b106-48b174b6c4a4
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: c480bede-ccfb-4384-acfc-9f79befa385f
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 66faf91e-285a-46d6-a54b-4b96ff10e60b
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 0751e281-5e06-4518-8f01-4611b7058828
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 33d9acd5-ff17-4650-8b6f-d6296544af43
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 813dd497-1d0b-462e-ba35-96448f1092bc
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: fbc99f73-5f62-4e10-8357-8706a3dcd3e6
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 5ea9be75-e5e1-4104-aaaa-cd380f7544c2
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 69cfe28d-ed69-4316-a83f-5e97fbf43f29
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: fbc6eb51-38c5-46cd-8a34-2c7b4c6f0797
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 3737917c-15e7-4623-8f9c-9f4c7ec9f055
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 3fb8b4cd-3341-425e-8724-53dfa94c1134
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 643d33ca-969b-4a05-bb5c-028d15824402
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 39e13163-d118-4e39-b731-2d85a9de1c1b
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 591319f4-2de9-44ac-b2ee-af2ff6631e24
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 70028ad1-c603-47a6-82a7-9bf699703290
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 8dd46dd3-549c-41af-b14a-7d6e2bb0cf3a
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: e81f81b3-1717-4bde-858a-c86fc72fbe90
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 5edd07e1-2215-43db-9540-69366b77ced7
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: c2d11ad5-ce9b-4d65-8610-77d32c22b7d2
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 17e201a3-4bde-45bc-8f62-15163b1f3f8d
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 485b44d7-1771-46f5-9662-a3032665f4ef
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 5348dc59-08af-4f30-9879-ef71f4c9765f
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 3b7871c7-b61c-4ecb-8673-1969a04ac9c9
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: f271b6ca-ae20-4803-9a54-4264ea474686
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 1cebd1b8-ff03-418a-b0bd-4b9806dbd650
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 36d545e9-a805-414a-a8f3-79affc854ecb
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: d2616b23-b0e0-478e-8762-ee6e8e53cf60
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: ed0fd309-60f3-4b35-8593-77a4401f2885
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: c93c012b-9b86-4a98-a3f7-85fcde902e78
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 9d9b82bd-4052-4b30-bebf-97dd806412bd
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 60688fcd-36b0-4c73-8062-19a7f86ac493
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 29ac1912-edb6-49e7-b70b-a95b19df96ec
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: a9132318-6a1a-455f-a029-d0f556b8d4ed
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: ffd814ad-c6ef-48d1-a2d3-0c9533c2740a
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 0cf7049f-eb21-4339-94ef-c80be2cd5165
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 4d63d53d-9b86-4f4f-9bfe-9db7c572add1
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 51924959-1195-422b-952a-2a165f9f02c4
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 84f54349-5cfa-4a9f-b14f-a5539afc357a
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 7efcaaad-7316-474f-aafd-91026aef1ddc
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: a82a4e35-749b-4d36-bcbe-75c7b29dd0ab
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 06a609b4-3757-49ce-b1aa-b904702d0e9f
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: b1cdad28-9a85-4eb0-8ffd-9ff3f6088e59
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: d57d5357-7f00-4f55-9a1d-3e884309ac4b
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: b6d7d48e-5f5e-4298-ab85-ca8ea65d1a88
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 3353971f-c39a-446d-b947-23e830547674
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 38d30b2e-1670-4468-9263-6439a0431618
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 250f9b40-4190-4ff6-b435-f576702cb541
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 59311bf9-de42-4049-b3c4-afca5c3f0dbb
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 104f8f21-da4d-47de-90ce-a5a2b73ab1bd
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 2748225c-4beb-42e8-9c5c-f0adefb99582
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: d2b2975e-c732-4a47-a181-1049fac0b9dc
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 8c1a80f0-0a63-4c04-86c1-296cd391503f
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: c5e5694c-a920-44f7-bf3e-30d82cfe13ca
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 80bfbab1-b01b-4851-bafc-80e207b96ba8
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: b0928fa7-aeed-45ae-b35f-187b7503ad3f
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: de102334-0bbd-4acd-bc92-0ed18d441b64
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: be5570f6-c807-49bf-8c2a-978521545812
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: f8ebb4e3-5b10-41dc-b140-587231561415
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 9d7030ae-c4ac-409c-876d-d0d59b6fdce7
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 1c1907a2-9908-4e87-987f-c1fab3bba1c5
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 9ff0d80d-de7a-418d-820b-de4e4fd213f8
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 7df21b21-d855-438b-ab8c-cd2b8dcf8b6a
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 9f7eb0ac-60d3-4afd-9f89-3124fe28d660
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 35f8e63e-95d5-40cb-809a-40af6d568afb
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: afd4b352-214c-43fa-8bc0-2d8575893f44
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 8b7a48d1-c7f4-4f59-b1f9-20e7f4c4aaf3
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 73d667d0-fb95-44e0-bd70-894e99226bb3
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: b44dd877-bb23-48da-9f02-ed1dae21749f
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 71561382-dac0-4f70-aca1-2b66bb873613
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 5ed199db-bc93-43dd-9802-a68c36b07755
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: a314d56c-6ebc-42dd-8ca0-0dec74e93d3b
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: ca34ff98-58c3-495d-b2d3-d2a248f301ed
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: 0ce65b9b-aebd-4f6e-a088-631efe58e603
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: fb31b365-aeab-4b69-b745-550e0116eb0e
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: b09733a7-ebe8-444d-a075-011b0f82f2b6
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    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: e3e7d5a9-f2e5-4fda-ae7d-c167782fb57a
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_valuebound50.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_valuebound50.c
      input_file_hashes:
        ../plain/dijkstra-u_valuebound50.c: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_valuebound50.c
    file_hash: 7ab48dd793c80bfdca8b2cb012b1dd7cd8eda625223788e3f60486b3a2e166d4
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: h <= 3221225469U
    type: assertion
    format: C
