- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f4486b23-fa06-40c9-bf6c-3bce8bd72fdc
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    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: 172120da-7e7a-4a5e-8ccb-54bc71a41107
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    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: 2040f122-96df-4c9e-908a-18dc367ac830
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    line: 28
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 37acd5aa-c110-4711-8953-91306101059f
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    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: 76adc419-4506-43a9-8a2f-fabeceacdc6f
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    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: deeddb6c-de32-4f99-a1c1-61c8e1d1ff95
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    line: 30
    column: 12
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 96e4c60d-610d-47a2-89b8-dd222931adf3
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    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: c6e10baf-2edb-437b-83e8-624cbbdc4256
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    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: eced2d59-5be7-44e4-a505-1e66ceccff4a
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    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: e104f932-286f-4455-ba30-25067dbf2618
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    line: 33
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 860d8c20-da20-42e0-b1a1-2a498081b826
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    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: cab85e11-e8e2-4042-8e4b-6e5d4d39f9bd
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    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: 06b78b65-6341-4365-b32c-62452a824030
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    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: d933bf02-78eb-4545-83b9-f3431fdd23ec
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    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: 8002a295-af3e-496e-beae-7810671f846d
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    line: 34
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 67f8c5f1-49ff-49de-bf57-6908ffd1d4ec
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    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: f40599f1-ebbe-44a9-839b-82b183fc3e16
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    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: 4a0b85e8-196c-40b7-8aa0-c06e749f0141
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    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: bb9f8bbc-e566-48df-b64b-a4a7e73e9280
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    line: 35
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 251edc1c-8fa6-40f8-ab7d-09b587c03e6a
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    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: 15f1cca8-2a11-48dd-93df-63752b38397f
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    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: 107be898-d2e6-48e9-abeb-2939d8eab225
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    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: 9aa51105-ee7b-4036-b337-2defe8bb9241
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    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: 5acd78c6-6ec6-4164-b346-cef8ca42cba4
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    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: cd74c6bb-1777-4f00-ac9f-5a356b81d5d3
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    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: 2b83f0be-cd1a-478d-9f3d-1f16e5284af5
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: counter <= 3
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a262a402-3bcc-4c69-a782-7adfde353c18
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    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: 248575f3-66a7-4d40-ac6e-69896f265bee
    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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps3-ll_unwindbound2.c: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps3-ll_unwindbound2.c
    file_hash: 60ff3152151a0df7365f100539e4b819551c378d98595a816ec37039149f1cc3
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
