- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c40ec956-5788-44d4-97ac-b2668649bcf7
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    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: 571a0f80-d707-4495-9860-c1f8f8351832
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    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: 5c5ac831-1d05-468a-9bf5-684d88ed55a8
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    line: 28
    column: 8
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bbdc748b-f6a1-43d1-94fe-6c954ed2d388
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    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: 61443a05-fd6a-4f2a-8421-d1120090662e
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    line: 30
    column: 12
    function: main
  location_invariant:
    string: c <= 32767LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c1a07eb7-750f-48d5-ae19-afee4acfa942
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    line: 30
    column: 12
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1903584-5c3d-4e36-ac76-27cbe8b9f42f
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    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: 226a795e-c0d0-48f9-a9c4-ba530f1a1222
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    line: 33
    column: 8
    function: main
  location_invariant:
    string: c <= 32766LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ce800652-47bb-44ec-ab2f-5a1bdc787d57
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    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: ffe2b432-2c4d-46e0-890c-54fb2fb41287
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    line: 33
    column: 8
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82257a65-7e5a-4180-9dc7-c2f66a5a40f0
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    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: 263d4e05-f806-4c96-8f22-c244a0f8a642
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    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: 075dd47b-683d-4c1d-a6bd-fe2f6f5dcf1a
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    line: 34
    column: 8
    function: main
  location_invariant:
    string: c <= 32767LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 428a4254-877e-46e5-94b5-394e4da893b7
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    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: b6fe5458-77a8-482d-a946-286f7e2cf164
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    line: 34
    column: 8
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef9be411-e01f-435a-8b4d-1efc0ce45e5e
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    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: ec27892d-9b89-4327-9098-096c1292b4ad
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    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: 3d8161a9-998b-4225-886e-2e5f0b7c36d0
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    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: d0acb349-1da5-4968-952d-f874cc183091
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    line: 35
    column: 8
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ab9b4e9a-d1fd-454d-81b7-d80292b2b5a4
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    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: 799a1be7-2aa2-4c3c-b184-fc2376dc7f05
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    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: 888a0164-1a3f-4d9f-80a7-e24eb87855fd
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    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: 8a9b87f7-1f90-47be-b3bd-4b6b38020d55
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    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: bb0af4aa-e99e-47b7-8956-8a5ddd8b2f26
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    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: 905ab52f-3432-4538-8dd3-deab7aa0fe83
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    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: d58f92f7-12f7-4cd3-af17-26b03505fcf6
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: counter <= 101
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 97403779-7a3b-4a46-b778-c02b91e070d4
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: c <= 32767LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 702dc0c4-258b-4593-8db2-481cba74fb65
    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/ps3-ll_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound100.c: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound100.c
    file_hash: baeebe831189d0208212eeaf417b83dac95cdcd24131565645f78fcbd5cf583c
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
