- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 232b3d3d-25b3-411a-95a9-45543951c673
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    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: 595edf72-1bf6-4970-903b-01882751bcfb
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    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: c2880e61-a160-409c-9e1a-c35df7505f05
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    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: bf42464a-4465-4bcf-ac11-8f09676cb7d1
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    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: 06202318-2079-406e-9d18-e1c1c191ed38
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    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: dfeedcc9-fe9b-4c5d-af14-94271a406bd8
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    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: 08ceaa57-666f-4333-a009-e8437ab4c375
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    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: 6ce31d32-979e-4313-b186-f726e9bee0ee
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    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: 4fc4434c-44b7-484d-a18b-a63f23fc8ad3
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    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: 1963da53-dd33-4cf3-b335-78c386d8f0f7
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    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: a800979f-1df0-46f8-8619-50842603cf56
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    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: 1464a914-1490-4bd9-a1a7-e1ba4de5e78d
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    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: ca369f7e-e9a0-41cf-a3a1-70c73039ef75
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    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: 8cfe9cd5-847e-4dc5-82b1-615d7d486cee
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    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: 96313b9e-08a9-4925-b556-4653f212eaf4
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    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: 93f3e419-8353-44b3-baf5-14cbf709a3bf
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    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: b3e6b077-ff32-46e9-9631-84323490e9fe
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    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: d2245472-ca18-4637-ac1d-781b229680c3
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    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: 4971bded-cd3d-4e89-936f-98018b2fc41f
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    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: 2f3aded4-4254-4b32-8f10-25ffd45df550
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    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: 84516cf3-0e6f-4a88-9d3e-2103dd1e39ea
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    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: 9ef5441f-11d5-4a14-ba9d-a34a1c18994e
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    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: a823eec4-fa40-4340-a8a7-14a47f6915c2
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    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: c8356240-0ef5-4b50-996c-89024eb11998
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_valuebound1.c
      input_file_hashes:
        ../plain/ps2-ll_valuebound1.c: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_valuebound1.c
    file_hash: 05d860f4c0b8d355d8344160864c48286246164c4c6e8e3a08816fe000adfcec
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
