- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b6f9fad3-9e89-4b43-a043-a08c175d475b
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    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: ab057976-cbb1-4770-82dd-74473315b3cf
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    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: 655d24b9-f9bf-44d0-b49f-0dde091b9999
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    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: 1c5364ac-26d7-44cb-9893-b98f80566245
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    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: 124f0454-bc56-4681-8f03-c4e30d53d60b
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    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: 9a9a027b-eff9-461f-a2d6-d8ea7649a52b
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    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: a35b371a-9825-4ccb-b0cc-637b39f84209
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    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: 6c7642e6-51ad-41b9-a35c-f0ae84bd22db
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    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: 733eb2b4-f29e-4557-bd76-7ae61beccafb
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    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: dc3972b8-103b-4b47-a53d-782624f97093
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    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: ba8d4c82-52f0-465e-9067-4f5aa9d41cb6
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    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: 92058760-398c-44ce-8732-9ab0ed3532d2
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    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: 5a31f920-27e9-4d8b-9e75-9a1400793a09
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    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: c0661e0f-7002-41b0-85f1-ba8d660b371e
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    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: 222e5229-6589-487b-9e86-58eaf6d05c61
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    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: df4a4d2b-f6c8-4b3e-9a14-ff424bcb0230
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    line: 37
    column: 4
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f62d7522-7d46-4490-8928-c94ade9800d5
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    line: 37
    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: bc1168a6-9dac-4533-9406-f02e6c92fff6
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    line: 39
    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: 9c48d148-83a6-46c8-8183-d94afa5736db
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    line: 21
    column: 4
    function: main
  location_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9c47ab76-59bd-4658-bee6-7ca50da75562
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    line: 21
    column: 4
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fd5773df-3e8d-447e-bea2-01b5aa51698a
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    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: 18ef6070-9d3d-4a81-bc5d-1890bdd34901
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    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: 88350c68-6701-4cef-bbaf-e04f16ff71b0
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    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: 58064eea-3851-4a2a-a413-474506696b75
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound10.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound10.c: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound10.c
    file_hash: 464ff86972962e190fa8e3bdd89b592f22b90512739ab3fd4df7709eb39adee3
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
