- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a631a26c-4fd2-409d-b2f5-067ead48ab43
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 28
    column: 8
    function: main
  location_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ece45d6f-5178-4cc1-a242-1e4ba39ad175
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 28
    column: 8
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9bf8a89d-3799-47e3-a6df-c243c19c63bf
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 28
    column: 8
    function: main
  location_invariant:
    string: 5LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 309a97e4-c7da-4d26-ae2a-40fceadfe9bc
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 30
    column: 12
    function: main
  location_invariant:
    string: 0LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 92dca760-5b2f-435b-8aeb-b7391d1b0c52
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 30
    column: 12
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cc4c5b1d-c0d1-4558-8196-8f9742f627e6
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 30
    column: 12
    function: main
  location_invariant:
    string: 5LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14d0c8f7-3a27-41b2-b866-78b7f64452f0
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 33
    column: 8
    function: main
  location_invariant:
    string: 0LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5adf8d25-da38-4ede-8bc3-b6ad13f59f72
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 33
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 94ef674a-ec7d-4595-91dd-89e39c2b3210
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 33
    column: 8
    function: main
  location_invariant:
    string: (-1LL - c) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d4ec1a8f-c9e8-4682-93da-11a410db1e8f
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 33
    column: 8
    function: main
  location_invariant:
    string: 5LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 26db68fc-9403-4321-be22-c4db57bcdecc
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 34
    column: 8
    function: main
  location_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c4832238-9c2d-40a1-b7b5-d8d043d83e86
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 34
    column: 8
    function: main
  location_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 12cb3085-2141-44c7-a37d-450e0a137a6c
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 34
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ede8e5f8-1627-4f15-94ba-fb28855316d3
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 34
    column: 8
    function: main
  location_invariant:
    string: (0LL - c) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d20c4786-b742-4e7b-8316-be89c869d359
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 34
    column: 8
    function: main
  location_invariant:
    string: 5LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b3ecf945-484a-43ed-b1b4-a0a2f72cb362
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 35
    column: 8
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1dbad45-9b3a-4b54-a42b-93bc64bafe3d
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 35
    column: 8
    function: main
  location_invariant:
    string: 1LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ed9c4bbb-be49-45e6-9802-a651ac1d2734
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 35
    column: 8
    function: main
  location_invariant:
    string: (0LL - c) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8f65af44-a569-4660-bfe5-f77c913a9b7c
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 35
    column: 8
    function: main
  location_invariant:
    string: 5LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e5c632d-d563-4195-b0f4-b0f656275895
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 37
    column: 4
    function: main
  location_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dabf136e-d62f-4311-8192-543627999157
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 37
    column: 4
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f734f8a0-81fd-4f83-826a-0ecc0c5d65c4
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: 0 <= counter
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 79e67d09-78db-4bff-8350-132b6f6be3ea
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1c09c08c-be8c-4791-a83c-8f030db9b418
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0f1dfb86-7cd6-4863-9b5f-65876a4b9064
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5f89099f-13a6-41a7-a5eb-212dbd1abeb0
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: counter <= 6
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fd819f1e-085e-4863-848b-d0b18981e689
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 75336a37-d032-48e6-b4ac-9033cfc8c34a
    creation_time: 2023-01-27T16:29:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound5.c: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound5.c
    file_hash: 03c4946022d2e6f710dd6221d8af6a4ec932dc09e858917dba12290a0f27caf9
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: 5LL - (long long )counter >= 0LL
    type: assertion
    format: C
