- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 45e8cc99-c7c3-41d7-8253-a187313ba74c
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    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: b996e5cb-14ec-4119-b37c-0d68bd0014fb
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    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: 03364514-f7ce-4c33-a7d0-ff4887a3608b
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    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: bd902bf8-e77f-4f11-94fd-b7c4540da48c
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    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: 747db66f-3122-4fb8-85a4-56979de004ca
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    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: 0f965522-a3ef-4634-a491-11b47df30551
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    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: f5d56a0b-de29-4cd2-a018-2e07a421829c
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    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: 53cf89c8-5265-4205-ac8f-3f05ece72cf5
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    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: 6475f57a-ca97-4566-80ae-1fe9d6b8a974
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    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: 91bb3a9e-ba91-49c9-962e-967547befe98
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    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: c716e717-7bd2-422e-a0f8-c7f40585493d
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    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: 56b21790-5d19-47f8-a9f6-90bac24c73ca
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    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: ade736b8-ea56-470b-af5a-373ad62e169f
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    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: 92d2566d-c658-43e8-aa22-654c16e36d77
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    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: e185dd5b-5d75-4495-aac7-4f3d032d9f63
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    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: 18f24801-ed5c-4858-ae5f-e861cc768511
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    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: 1b2f97f8-b9d6-4a3d-a60c-e4e775bbf656
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    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: 4813126b-9041-4352-b776-47099bb2495f
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    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: b3992e76-3a9c-43cb-9379-9629461f62cb
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    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: 94148f02-9dee-46d3-8374-78d6f91d038b
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    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: f232156b-406f-431d-ab8c-0b110f0e319c
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    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: 657a5a2e-6d1b-463f-89e5-2451656dad09
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    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: e2c320b6-8cb0-41e4-94b0-67e6ce305d40
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    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: ab3e0df3-fd68-4787-82ea-787c4c76103a
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound5.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound5.c: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound5.c
    file_hash: 1b50d522769b95768e9038f61a48a3b927d40a7b91b44cb14af45fcd08759b69
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
