- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0904c363-4858-4306-8f1d-86bbcb22f0d6
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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.c'''
    task:
      input_files:
      - ../plain/ps2-ll.c
      input_file_hashes:
        ../plain/ps2-ll.c: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll.c
    file_hash: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
    line: 27
    column: 8
    function: main
  location_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8a919b3f-8b63-4827-b7a9-54f0251ee793
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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.c'''
    task:
      input_files:
      - ../plain/ps2-ll.c
      input_file_hashes:
        ../plain/ps2-ll.c: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll.c
    file_hash: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
    line: 27
    column: 8
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1aaa5d6-ac98-4a28-b706-141d1d07dcb8
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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.c'''
    task:
      input_files:
      - ../plain/ps2-ll.c
      input_file_hashes:
        ../plain/ps2-ll.c: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll.c
    file_hash: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
    line: 29
    column: 12
    function: main
  location_invariant:
    string: 0LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2707cb4b-b900-4b20-9cdb-382178e13617
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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.c'''
    task:
      input_files:
      - ../plain/ps2-ll.c
      input_file_hashes:
        ../plain/ps2-ll.c: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll.c
    file_hash: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
    line: 29
    column: 12
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 40d1f402-ea1e-497f-8471-f7dbc13a8c4b
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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.c'''
    task:
      input_files:
      - ../plain/ps2-ll.c
      input_file_hashes:
        ../plain/ps2-ll.c: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll.c
    file_hash: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
    line: 32
    column: 8
    function: main
  location_invariant:
    string: 0LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c03275b-21ff-4d2c-8d9e-9bb2d5c79ca8
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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.c'''
    task:
      input_files:
      - ../plain/ps2-ll.c
      input_file_hashes:
        ../plain/ps2-ll.c: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll.c
    file_hash: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
    line: 32
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: beaf8dc9-006c-41c7-8ece-81d08fa9e273
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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.c'''
    task:
      input_files:
      - ../plain/ps2-ll.c
      input_file_hashes:
        ../plain/ps2-ll.c: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll.c
    file_hash: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
    line: 32
    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: 4b413b4b-af59-42b9-8043-b6d547d57e5a
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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.c'''
    task:
      input_files:
      - ../plain/ps2-ll.c
      input_file_hashes:
        ../plain/ps2-ll.c: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll.c
    file_hash: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
    line: 33
    column: 8
    function: main
  location_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2bebeac3-7829-47be-a369-8f6e4f1d5a74
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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.c'''
    task:
      input_files:
      - ../plain/ps2-ll.c
      input_file_hashes:
        ../plain/ps2-ll.c: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll.c
    file_hash: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
    line: 33
    column: 8
    function: main
  location_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 029aa0f9-38f4-4e24-8ee3-f3e761d6d8b4
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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.c'''
    task:
      input_files:
      - ../plain/ps2-ll.c
      input_file_hashes:
        ../plain/ps2-ll.c: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll.c
    file_hash: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
    line: 33
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0d817da3-8c0c-47d4-8d4a-34ba598c6d55
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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.c'''
    task:
      input_files:
      - ../plain/ps2-ll.c
      input_file_hashes:
        ../plain/ps2-ll.c: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll.c
    file_hash: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
    line: 33
    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: a24f07c6-4b7f-415c-8d3e-85ea69be97ac
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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.c'''
    task:
      input_files:
      - ../plain/ps2-ll.c
      input_file_hashes:
        ../plain/ps2-ll.c: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll.c
    file_hash: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
    line: 34
    column: 8
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a3a27e9-3af1-4c05-a8aa-c0c2f49fcb23
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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.c'''
    task:
      input_files:
      - ../plain/ps2-ll.c
      input_file_hashes:
        ../plain/ps2-ll.c: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll.c
    file_hash: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
    line: 34
    column: 8
    function: main
  location_invariant:
    string: 1LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dd1ed41e-eed3-4c7e-b9b5-6dc560bdaa00
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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.c'''
    task:
      input_files:
      - ../plain/ps2-ll.c
      input_file_hashes:
        ../plain/ps2-ll.c: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll.c
    file_hash: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
    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: bc61d689-a4eb-44f1-8353-62e5e1709266
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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.c'''
    task:
      input_files:
      - ../plain/ps2-ll.c
      input_file_hashes:
        ../plain/ps2-ll.c: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll.c
    file_hash: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
    line: 36
    column: 4
    function: main
  location_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b45c218-84bf-4b76-93aa-ebf1a42e7aad
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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.c'''
    task:
      input_files:
      - ../plain/ps2-ll.c
      input_file_hashes:
        ../plain/ps2-ll.c: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll.c
    file_hash: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
    line: 36
    column: 4
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 23b82752-a27c-41cd-842a-a88520fc5002
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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.c'''
    task:
      input_files:
      - ../plain/ps2-ll.c
      input_file_hashes:
        ../plain/ps2-ll.c: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll.c
    file_hash: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
    line: 36
    column: 4
    function: main
  location_invariant:
    string: c - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2105f373-5073-4e86-901a-0131ce2ecedd
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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.c'''
    task:
      input_files:
      - ../plain/ps2-ll.c
      input_file_hashes:
        ../plain/ps2-ll.c: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll.c
    file_hash: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
    line: 38
    column: 4
    function: main
  location_invariant:
    string: c - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f1ed4884-e980-41a2-bd7e-a7def1952b4f
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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.c'''
    task:
      input_files:
      - ../plain/ps2-ll.c
      input_file_hashes:
        ../plain/ps2-ll.c: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll.c
    file_hash: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 020f8fad-97fd-49cd-9057-63fa048b1dd5
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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.c'''
    task:
      input_files:
      - ../plain/ps2-ll.c
      input_file_hashes:
        ../plain/ps2-ll.c: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll.c
    file_hash: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ad9a7aba-9aca-40ac-b387-dfe4b538ba96
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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.c'''
    task:
      input_files:
      - ../plain/ps2-ll.c
      input_file_hashes:
        ../plain/ps2-ll.c: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll.c
    file_hash: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 96e74b53-d2ce-4fea-b8ce-f330047858fa
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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.c'''
    task:
      input_files:
      - ../plain/ps2-ll.c
      input_file_hashes:
        ../plain/ps2-ll.c: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll.c
    file_hash: 179b0134270d97f57074f9ac11d0788729a2f9ba65b60cccc5fdcd06091925db
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
