- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7317f215-1891-4fa2-a628-0df8539aa120
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    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: 1a59fc64-08ae-4c62-93b4-362476b1b9d1
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    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: cbb04410-896b-4354-9439-f52d29846e7e
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    line: 28
    column: 8
    function: main
  location_invariant:
    string: y <= 1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e730c46c-23e8-43f4-827a-d58f021a8b5f
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    line: 28
    column: 8
    function: main
  location_invariant:
    string: x <= 1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ae71f6a-7bd4-4faf-bb96-94132d2bb300
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    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: 81360330-36fb-4872-a715-0627ae1cf11e
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    line: 30
    column: 12
    function: main
  location_invariant:
    string: c <= 1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db57cfc3-6689-41f8-9d34-9f808671c58d
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    line: 33
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f5c46d8-6fec-473f-aa34-ca1b1094dca2
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    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: f7a42cec-857e-4676-a441-caa22fc15440
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    line: 34
    column: 8
    function: main
  location_invariant:
    string: y <= 1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d0a90258-86b3-4d35-b8ae-72dba51380aa
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    line: 34
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7df94dc5-6c9d-4693-9109-7ddf17d7442d
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    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: 1b18e783-4e94-4ae1-bf5e-086c69a0cace
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    line: 35
    column: 8
    function: main
  location_invariant:
    string: x <= 1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ff77f655-607d-4c2e-a41b-c019ab502958
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    line: 35
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 883e8c70-e5b1-4736-8ca9-e1725d4e8a8e
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    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: bcd31364-c814-4ce1-9900-54fd43e43e8f
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    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: b427bc4d-25d7-4e0a-991d-483bdb9d8ea6
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    line: 37
    column: 4
    function: main
  location_invariant:
    string: y <= 1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ce1beb9-2f49-4426-9d82-a3c3b799dd36
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    line: 37
    column: 4
    function: main
  location_invariant:
    string: x <= 1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1885f4e6-7e70-4979-8883-337ee5793af7
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    line: 37
    column: 4
    function: main
  location_invariant:
    string: c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 372b7ac2-e7e2-4f7f-8794-47382b54f14d
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    line: 39
    column: 4
    function: main
  location_invariant:
    string: c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0cfd866f-c40a-4ed4-8c26-7cefd8a2d19d
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    line: 39
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 59389712-5ac7-458d-a476-87b7a6677dee
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    line: 10
    column: 8
    function: __VERIFIER_assert
  location_invariant:
    string: -1LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b6887692-9459-43e8-802e-54dc341f9508
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    line: 12
    column: 9
    function: __VERIFIER_assert
  location_invariant:
    string: -1LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8ebeefb2-2f53-46b7-a38e-519feb439686
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    line: 14
    column: 4
    function: __VERIFIER_assert
  location_invariant:
    string: -1LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d9aec773-e571-4822-ae9a-30862e84a23d
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    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: d535749a-102c-4ff2-8c90-c4e5f195d1b9
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    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: a121b47e-c59b-4f5c-97c5-5ebb6a601c68
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    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: 73c5a6b3-5d6e-4418-8f77-0fb75125374d
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    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: 7ecf5e61-b8bf-45ba-8016-fdabe6ed9d6b
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: counter <= 2
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: aa8db770-3d60-4d2f-aeb3-861974cbd9e2
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: y <= 1LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c2b147b6-96aa-41ef-bf79-b95ec5846e7c
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: x <= 1LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: af3a5b45-fa7e-476c-ab37-a8df6967b38f
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: c <= 1LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1cf27fa9-7b7b-401d-943c-23096cc62159
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: caf041f6-5900-409b-948c-c2deab2e515a
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound1.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound1.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound1.c: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound1.c
    file_hash: eeab39c4b0b140806b3ddcf9e96fb8e36f66c5baac57da41aaf4e88167e6b080
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: 1LL - c >= 0LL
    type: assertion
    format: C
