- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 366c0f47-923f-4dbc-8a08-247e97d91dd6
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 31
    column: 12
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 069c8238-964e-455e-adcb-a08b185a61ff
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 31
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e610bb42-077d-4ff3-a177-c511a3f388d7
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 34
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: caa7e09b-3ca9-4205-85e9-212f4b86f158
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 34
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a4d17eb5-fad9-4bba-bd07-4b89c8ef811b
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 5494ec7d-65b2-4f4b-95cd-e49d3ca5df24
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 39
    column: 8
    function: main
  location_invariant:
    string: p <= 3221225470U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7976008d-7dcf-475d-b2b4-fa6e6d4d802f
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 39
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 76f496b9-6eaa-4aa4-8301-d6ca906722ea
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 39
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 03046e3f-760c-4850-991f-13dc332ca34b
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 40
    column: 8
    function: main
  location_invariant:
    string: p <= 3221225470U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b2af86a-0c46-4114-9f46-f351622276fe
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 40
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f479f44-970d-43b8-8957-568e717b95a5
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 40
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ac876895-262c-4936-996e-d6ad64beb412
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 41
    column: 8
    function: main
  location_invariant:
    string: p <= 3221225470U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f8c0afab-0c4f-4ed5-8548-70f7cc54e86c
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 41
    column: 8
    function: main
  location_invariant:
    string: h <= 4294967293U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e4028cb-fb13-479c-9ce6-6faaa4c95968
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f791c395-4017-4146-9d5f-2e8d6a99bc8c
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 571d98db-24d2-400e-9e14-91ad0ee3e07d
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 42
    column: 8
    function: main
  location_invariant:
    string: p <= 3221225470U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf9220a9-ac51-4a85-b864-f24994fb5296
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 42
    column: 8
    function: main
  location_invariant:
    string: h <= 4294967293U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fa1b1932-0538-4fd9-bcda-26a3db234694
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 42
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2107239c-2f5a-4050-920e-25a8d9d728b7
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 42
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fc70a6a1-b634-4c27-801b-27781a9c57f0
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 43
    column: 8
    function: main
  location_invariant:
    string: p <= 3221225470U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82929c71-9e09-48b0-a186-0a96c150f768
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 43
    column: 8
    function: main
  location_invariant:
    string: h <= 4294967293U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f6d38fac-b4a5-4097-9a7c-28a1850c3ab4
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 43
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8705e450-b94c-4de3-941a-282fc9b0eca6
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 43
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 345758a6-2868-4809-b44e-a8d6a77b9a48
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 44
    column: 8
    function: main
  location_invariant:
    string: p <= 3221225470U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b2d453f9-0237-4d2e-8c16-ca03b3ee0142
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 44
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c49fb91-b1bd-4de9-b915-63ba85c026a7
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 44
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a00d7b55-b76e-4772-a6b2-9a5d95ed853f
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 46
    column: 12
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9cfbedaa-80e1-4945-9919-98ef1024eb1b
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 46
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 29d014ac-0a1c-4617-b994-7396f64b755d
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c
    file_hash: 202bef7949e13bb96f32c25afbfc6c3ab25ae2d31d5e937a54fdffa4785c5a47
    line: 43
    column: 127
    function: __VERIFIER_nondet_uint
  location_invariant:
    string: 4294967295LL - (long long )val >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1eaeaab8-86b2-47ff-8a36-8dbc27800c5f
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c
    file_hash: 202bef7949e13bb96f32c25afbfc6c3ab25ae2d31d5e937a54fdffa4785c5a47
    line: 43
    column: 127
    function: __VERIFIER_nondet_uint
  location_invariant:
    string: (long long )val >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 84b90261-8b88-4120-8d1e-5ea4306653a3
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 49
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82d41881-e704-4b31-8e38-c86fd7b3a7ee
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 49
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 177b1c5c-c220-4eef-b133-971f38a77f49
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 2145b0ea-b43a-4793-9e9b-0971e248d3b7
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 50
    column: 8
    function: main
  location_invariant:
    string: p <= 3221225470U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 12730de3-f87c-44bf-9a58-c4f53bef2b3f
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 2532301d-b1e1-44e0-a49c-7c00ea7bd969
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 50
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 29a8ae0b-6bc0-4856-9aa1-ebc4a31ecbd7
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 50
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f9b04ce0-8b87-47e2-9199-9f7ecdb50917
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 51
    column: 8
    function: main
  location_invariant:
    string: p <= 3221225470U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2fea7bc5-fbfd-4ba5-87db-b8e044bb0d54
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 51
    column: 8
    function: main
  location_invariant:
    string: h <= 4294967293U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a619fee0-4fcc-4cf5-a048-ae1f9255e23f
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 51
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d86556c5-f9bf-49dd-9f2f-0a698044ff9a
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 51
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: acf8aa96-bdb8-4f43-92cf-3f91cde2598d
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 52
    column: 12
    function: main
  location_invariant:
    string: p <= 1610612735U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5b3e15bd-8fb3-4b41-87a3-88b9789f8292
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: e9520f44-736d-40d7-89bf-1ee2d146f416
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 52
    column: 12
    function: main
  location_invariant:
    string: h <= 4294967293U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 435c3028-9fb6-4461-ba97-0706be01b4fc
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 52
    column: 12
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 18c7698f-127b-4492-b7a8-90e5849d41d1
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 52
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 047255f7-1638-4bb7-ae96-3ce4198634ea
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 53
    column: 12
    function: main
  location_invariant:
    string: p <= 1610612735U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 304351c3-636b-46f1-8a5e-a404735e6ea5
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 413e9a46-ca9c-4da7-ad29-53a7703ebe8f
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: a37c28b1-4e0d-4bea-984e-26ce04daea25
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 53
    column: 12
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a5309d31-acfc-4c0d-a5e8-6477295dfdfd
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 53
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8f62bdd9-c029-4661-a342-85fc28d5d81f
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 54
    column: 12
    function: main
  location_invariant:
    string: p <= 2684354558U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3c9a885-2f0e-4841-9de6-774d641f2fa7
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 7c2856e0-d204-4505-9d07-f494d743a105
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 54
    column: 12
    function: main
  location_invariant:
    string: h <= 4294967293U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 64f8e48d-b107-4719-868a-bb91fb999d87
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 09ec4fcd-1bdf-402d-95e6-14fc0c287801
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 54
    column: 12
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f0ec0c32-4318-49ba-a454-8dfd6c02cafa
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 54
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 15707c81-79f5-4e79-b457-66545c0b1e13
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 57
    column: 4
    function: main
  location_invariant:
    string: p <= 3221225470U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c6391ab-2d14-4979-b28e-b24b59d6c009
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 57
    column: 4
    function: main
  location_invariant:
    string: h <= 4294967293U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 71e56dd4-f2f2-4091-92fc-57c077324d67
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 57
    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: 4e823320-47f2-4573-af00-2eee8e957821
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 58
    column: 4
    function: main
  location_invariant:
    string: p <= 3221225470U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5cb87a30-984c-4bec-8603-449e0f72f00a
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 58
    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: 0664feca-ad36-4ea2-9c85-9d9d7d62d78c
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 59
    column: 4
    function: main
  location_invariant:
    string: p <= 3221225470U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: acc403a6-9f8a-43d0-ac5f-6dccbb857a03
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 59
    column: 4
    function: main
  location_invariant:
    string: h <= 4294967293U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 933b6cfe-3596-42b6-b734-080466f6fa5e
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 59
    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: 3902daf7-9675-40ee-977c-ae1ff8f143ff
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 60
    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: 5353b32b-9e12-4947-ab2d-076f0d565090
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 740e4a8a-fb92-4ad8-afec-d9e17046700a
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 007bcb8c-ddf3-472d-9205-9dffe1a8a590
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: e1efd353-f217-4d06-a62e-3d26b943a8c5
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: f7e84c6f-2e5f-4096-8432-ee81ac3a4fcd
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 4ce11463-49cc-495b-9f97-a3df0b449419
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 87b78a88-ebff-461a-9fa2-56d53c796918
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 6af4d439-bc80-4036-8781-30646a3cbefd
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 26cfd0bf-1a56-4352-b43d-6101c12267e5
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 31cce4c8-256a-4500-8427-202294331718
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 23
    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: c8c754e6-7fc2-4e54-a8ab-0dad2ae0cbab
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 24
    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: 95200d73-7f27-48b5-b476-d3d2a4f9289c
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 01287926-b31d-4f57-a6d8-d904139d4e47
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 789370f9-d1c8-445d-a3c1-1d1e63d906fb
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: aeed5c7b-c1e8-43d4-b948-9387f6a4be86
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 4fced498-fa43-4f5c-9a58-5887d35a7261
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 24
    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: 62f9392f-1121-483a-8e17-6628b7512e44
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 5063d528-0c0d-4288-8721-7e88b34c3dbd
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: a490ef32-e4f9-4d5b-b634-4ec44216ac10
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 7316172e-aec6-4741-a90f-2a6082408c48
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 3cc79970-13c7-447d-98e8-0802ddc68f0e
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 26
    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: 854ef240-4e97-40d8-87a5-51038338627f
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: f2819ac9-7861-45de-9c87-f40fbc5f5553
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 3d6c8881-16f3-436c-88e4-e6a7341bc9fa
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: a7500f87-62b8-4b7e-91a5-175f9727db3d
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 55fe82e5-d7ff-49f6-b1f6-59cb05cf0909
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 26
    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: d31636d3-c1dd-40c1-bf6b-1f0cbc637b3e
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: f30704c0-5f13-457d-8e65-fd0f5da331c7
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: a4e27a2b-8ea7-4454-bc9a-df663b414679
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 14e45b61-5082-4cc1-8a4a-414527fd6445
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 2911aadc-fed5-40dc-9471-e2f12758e7df
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 27
    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: ff0465b7-114a-4756-92c0-0800d4204e14
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 8c57d013-65cd-4bae-9867-2fdcee57863b
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 6ec0eec6-8065-4c90-92e7-077d215d60b0
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 6333d02c-f96d-4a93-ad72-8e0ccffa3f36
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 27
    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: 01ca0da6-4614-4bd7-9df5-990ae2681a65
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: b043c422-e9a9-40ca-a2f5-2fa577b1f430
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: c5f6beda-c642-4f95-967d-696e7c6c6f12
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 2e1c9d66-b7e3-478d-aaca-cabbc4d205b6
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 28
    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: 351e84a7-4e96-4010-991b-45f92249dc9a
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 6b946bca-8352-4cf0-b443-afd7998b8014
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 69477ec5-c8e3-4c7c-bfb8-f6c41df207c2
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 28
    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: 126a2d6c-550e-4b81-92a9-b2cbc950e68b
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: 918806e3-5b8c-4c7c-b72e-72606cc1f9b7
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: ead263f6-9c02-42ff-a99e-ebf8eb272275
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 29
    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: 69e96f6e-17f2-4b2c-bec1-2421ea3f1959
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    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: f364691e-db7f-48a3-b979-ec012618ecfe
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 29
    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: 3958008b-3028-46a0-bfbe-132530a8b74e
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 29
    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: d4b8b0e7-3070-4d0a-81d3-77f4251f44dc
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: 0 <= counter
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 12a8e7fe-3fea-487b-9726-5731f3447522
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: counter <= 3
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 26d6f999-21fa-4812-bbb8-47e0c134c486
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8f094e2d-6dc2-4c58-905b-a1fb5ab0affe
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 84a09bbe-2d4d-4981-b893-767197de13e8
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: 1 <= counter
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f16881b2-ad0e-4b13-98da-da7988641fbc
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: p <= 2684354558U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 40d72ec9-143d-494e-845f-e26c3f39e6dd
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: h <= 4294967293U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2aaf29f9-44ea-4fe9-b2de-d56f127f6868
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/dijkstra-u_unwindbound2.c'''
    task:
      input_files:
      - ../plain/dijkstra-u_unwindbound2.c
      input_file_hashes:
        ../plain/dijkstra-u_unwindbound2.c: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/dijkstra-u_unwindbound2.c
    file_hash: ee8fbf7ad7c769bb660b4c416c89e8a6070f0c88820552e25f4a5ca5398fd5ca
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
