- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4586da00-98fe-40ff-abd6-443cac200a3d
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    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: 662f5dd8-3f68-4f38-910c-8e356faccc04
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    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: 32053e2d-7922-422f-b3d9-ddf233c2eb40
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    line: 28
    column: 8
    function: main
  location_invariant:
    string: 50LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 93bfeae7-c2a3-4184-86f7-41e2811ebce5
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    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: 7f762e1a-2142-465b-88e9-d94703f98f56
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    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: 4f2801e4-773c-4246-a5a6-f1c6326c4134
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    line: 30
    column: 12
    function: main
  location_invariant:
    string: 50LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 54370bae-135d-4a6f-8538-f1794be609f4
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    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: d82f3965-debe-4535-a34e-12ca38587e40
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    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: 96f74aba-38e8-4c7d-97b1-8d2bbb99a3b3
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    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: bf9bb512-ab01-401a-a3cb-4922d3f8c21a
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    line: 33
    column: 8
    function: main
  location_invariant:
    string: 50LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d7fcfe2-c7de-45cc-addf-5e29fd04b984
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    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: e0dc204f-c0ff-45ce-9d4e-81845212cd6f
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    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: a963e533-7773-4bde-9b1f-eb9ca79d4050
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    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: 39f9f904-a95b-4e9b-89b7-9c3282d4c579
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    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: 09009295-baee-4741-b330-2a7533acd3a0
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    line: 34
    column: 8
    function: main
  location_invariant:
    string: 50LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b2a7fc0-bcf7-4771-9894-db5dce42ba29
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    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: 1743d37a-f70b-4b36-8b6e-d0a812cb7731
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    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: 0bbc998b-f07d-42bc-bbf8-f04c9a679d46
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    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: ab9f5518-42a4-4157-bec5-85b7584308e8
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    line: 35
    column: 8
    function: main
  location_invariant:
    string: 50LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cd4732e5-31e2-427a-a55a-e9d57236dd35
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    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: 8415aa23-ab93-47a0-8b85-388003233c4e
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    line: 37
    column: 4
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 34201f0b-f25d-459a-a59c-56a291e0ff52
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: 0 <= counter
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a606606c-03d3-453a-8846-8dc7c0e26d82
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    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: 2b957249-330d-4f5e-be10-6943a08e9eea
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    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: c83fc8ae-48b1-4bb7-9bf9-408a475a7dd2
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    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: 0ae8d653-0221-443d-8662-0ced8d95aa13
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: counter <= 51
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f15fa45f-d2a1-40a0-803f-6feb537b2f2d
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 449151a3-172b-413e-9160-2e53af2121c3
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound50.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound50.c: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound50.c
    file_hash: 82dba59912342fc33baf6f71838a6b7d05440c02338f64f7b1e8151e293c49a7
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: 50LL - (long long )counter >= 0LL
    type: assertion
    format: C
