- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 399f4fdc-3cb5-460d-8cc1-980a72602c7a
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    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: 4f45ce0e-53d3-43dc-abe7-02cb05c1d571
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    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: be33dea7-9332-4af9-ab89-4525e170c572
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    line: 28
    column: 8
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b18dafca-0109-41bf-8da3-763d8c118051
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    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: 93b88ff8-36e7-445f-a34f-89734dff3af2
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    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: 8b4a4505-23ee-4e0d-82c4-4be2ccf9ce4d
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    line: 30
    column: 12
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2620a6c4-aec0-4eeb-ae0b-2e27032243e4
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    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: da4a14d7-ea54-4cdd-b97a-0c1f2162618a
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    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: 4a4bd950-e7cc-4bfc-9147-f9f139ef6b17
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    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: a7964065-bd02-4e05-9af7-ab21bb00d08f
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    line: 33
    column: 8
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: efbf295b-1026-4dc6-8035-cd11ec67c3e5
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    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: 6f91736a-87fa-4210-bbe4-861436ac0b47
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    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: 1c93f13d-7379-4b8d-a996-c3b711eff974
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    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: f717918c-de46-4cc3-8774-9a0c5c7df893
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    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: 17187314-4de2-4109-898b-431dd40a8c8b
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    line: 34
    column: 8
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f7cf5289-cd27-46b3-b10c-8c7744ab49ad
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    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: 55dad801-e317-4b67-8fd4-71c402c7df39
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    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: f805414a-4034-4c66-9193-2830e7a8661a
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    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: de918ef5-7d46-4ffe-94ed-858fb725329c
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    line: 35
    column: 8
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43c0dd44-ff5d-4480-8e26-40b2ae897f73
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    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: af2a6679-d575-421c-9c44-8e2b4644ee63
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    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: 854b1554-e078-4e4f-9603-f5bef8f3502a
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    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: ba3e98d0-61d3-410e-96c7-9e810a1ecd49
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    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: fccc7c28-79ba-47e3-a5d6-f70fa517275c
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    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: 5132f070-70d5-43b5-a6f2-e0094a03714b
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    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: 47b42557-0dc0-4f51-bd8a-a198fa4a473a
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: counter <= 101
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e439331-f88d-4b24-84e2-0194883987f3
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    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: 483e7791-2e2d-4bb4-8db4-ea2806bc8332
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/ps2-ll_unwindbound100.c
      input_file_hashes:
        ../plain/ps2-ll_unwindbound100.c: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/ps2-ll_unwindbound100.c
    file_hash: 9dd084b74d402040bb1dcf601a4c548e70d932326201e2bbf6bd431598d05766
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
