- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5cf797d9-129e-495f-8760-198841b3ac95
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    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: b5285170-b588-426b-ab69-11e76a0c40d9
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    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: 0d87a86c-2f00-4649-9cf1-696cdee9de55
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    line: 28
    column: 8
    function: main
  location_invariant:
    string: 5LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 127a78b6-7221-40c6-b126-b9aa37407499
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    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: 50e83f6f-10f5-4de4-8ce6-0fcb7d9b1a28
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    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: 325709e2-14e2-45c3-92b4-50355d075097
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    line: 30
    column: 12
    function: main
  location_invariant:
    string: 5LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ac405eb2-1f7c-4cef-a234-74d4caecc870
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    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: 8b28bcc6-8b19-4d1f-bbfb-d8058b5f5581
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    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: 5e6bf938-f079-4a64-a851-06b521edc818
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    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: a9e4054e-24f4-45f9-8b6d-b830d3f204f1
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    line: 33
    column: 8
    function: main
  location_invariant:
    string: 5LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 98ec0f32-81da-4ca3-9f42-c3adb97082d2
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    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: 691f26f7-69a7-473e-8c75-fb52f603e6f2
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    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: 06c06f1d-f6e6-4030-b789-8dea9f801ea4
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    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: d8f7070a-58bc-4e0d-a97d-838dd9c2cfe0
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    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: 67fb2f0c-de1a-4216-9c17-331e894618bb
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    line: 34
    column: 8
    function: main
  location_invariant:
    string: 5LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1701d622-f5fa-4d30-b20b-04c8eb5349fb
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    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: 31484278-01f2-4afc-af35-2bcb9fca0351
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    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: 25135a1d-3fa2-4bf5-9a9e-1b0940e81367
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    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: 851ba1c6-4b89-4f1f-9cf1-bf3014ed4621
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    line: 35
    column: 8
    function: main
  location_invariant:
    string: 5LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c0f1205-e881-487a-b6a9-c2ae9e7053f2
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    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: 70c52fc3-1f24-4a08-bd4c-d349ea25337a
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    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: a2a7d453-82b0-48ce-9d37-bee1c4744cbe
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    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: c71aa71d-b2e9-47b0-b776-ed3f2c2fc792
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    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: 1211ff32-0941-4c48-b3c8-2fdc3e9c1de4
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    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: f25e6b92-735d-4ddf-89c8-0cacca8205f5
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    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: b31c6891-ed2c-481d-94ff-b4943209c259
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: counter <= 6
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6df32eac-ba2a-42ec-ac2a-28ca372797e5
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    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: 54c2c10f-a9c6-483e-a7b8-db94d788e215
    creation_time: 2023-01-27T16:29:49Z
    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_unwindbound5.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound5.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound5.c: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound5.c
    file_hash: f6f262ee8ef73ce794ec50b2a6144e291b9346fae74936a8743567d685b8f10f
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: 5LL - (long long )counter >= 0LL
    type: assertion
    format: C
