- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ae0ff320-00e1-4bdb-8e69-e8fe330706f4
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    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: e92d8df3-f0c0-415f-b95f-3ce02ff696c5
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    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: f3784006-3702-4f05-8eb7-d3f8f6ecf5b0
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    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: c98cf840-8eaf-4225-97f7-813522d8ec35
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    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: 066d753e-daf2-4c2e-aa8e-e6ba32f5588b
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    line: 30
    column: 12
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 35e31aeb-d6c5-42cc-821f-59686a3bb167
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    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: 2f52413a-909a-4565-919b-0657236bdbe6
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    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: 7a8b861a-f638-4103-b160-79108ab80d03
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    line: 33
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 548a680d-b600-44b5-bec6-7f4bf7569fe6
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    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: 6da416ad-377d-4c9c-9490-6e53154abad4
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    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: e747b6be-a2d8-471d-b4f4-b55b4bf647a9
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    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: 179bd96a-e3fb-4ac7-a140-aec153607f5e
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    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: 98953f12-4302-4e7d-9eef-d647cbfcdae8
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    line: 34
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c15fba8b-c288-461c-b0ad-0ce75666013b
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    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: ce8fadad-1818-453b-bbad-82dbe8572c2d
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    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: a5532395-7e09-44e8-97c5-6355c363aaa0
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    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: f4b795c9-1e7c-4c8b-bac2-31805ef116b3
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    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: 70fb303f-2b74-48d7-9c7e-020c6419853a
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    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: e8e90fa2-8b78-432d-9fa3-7b7e798f55ce
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    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: 3773c9e0-15bb-4d35-9589-0863a463743d
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    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: 77dfcd89-c72a-4443-99a9-867ec2cc87bd
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    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: 0f75764a-f6fb-4c9c-9872-bf39115aa06c
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    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: c03b0a63-9b91-47a0-be5f-2a581692e3bc
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    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: 9748e875-3e33-43b1-871a-4b244affe94c
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    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: 5a9a9468-ac98-47a6-8338-851ffae195b4
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    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: 1a5e5fe6-8be1-4606-89c3-3dfe716099d1
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    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: 2b9137fe-5dd7-476c-9b8d-8e9b6cea2863
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 797568d6-93f2-4ae0-97b8-2d21d1b03cc4
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/ps2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound2.c: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound2.c
    file_hash: 68a1d90e377c3311d76daf952c7a82207c21975afd6ee262fe642de3486ccf46
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
