- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 26c8971b-a3ed-45c3-899b-76ce1d7db09e
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 35
    column: 16
    function: main
  location_invariant:
    string: (-1LL - (long long )j) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6b40466c-423d-4520-b172-79d9c5e88b16
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 35
    column: 16
    function: main
  location_invariant:
    string: (0LL - 2LL * (long long )i) + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c5e9d975-24ef-4a47-bdfa-d0af6007fbd4
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 35
    column: 16
    function: main
  location_invariant:
    string: 999999LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e8014b9-0b9f-44ef-8db7-e00d1de38cff
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 35
    column: 16
    function: main
  location_invariant:
    string: (long long )k - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b7019c20-18db-41f0-ba3e-b7245e209dcf
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 35
    column: 16
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bc8b4616-ee46-448e-824c-1d2d6a7c8659
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 35
    column: 16
    function: main
  location_invariant:
    string: (-1LL - (long long )j) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 76cad4ad-e6b6-4801-bb15-6052d26b42a1
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 35
    column: 16
    function: main
  location_invariant:
    string: (0LL - 2LL * (long long )i) + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aefc6e8b-b37c-4a97-bc0a-48cab30dfaae
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 35
    column: 16
    function: main
  location_invariant:
    string: 999999LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82ea070e-dd2d-4413-9a1e-6186f122be2d
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 35
    column: 16
    function: main
  location_invariant:
    string: (long long )k - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f1c35ef0-7c44-408b-af0b-f21b10333237
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 35
    column: 16
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 93e5e28f-8c71-4fec-84e7-af240254f31d
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 37
    column: 20
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c497c2c5-2e34-49dd-8d89-bd626a9acd08
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 37
    column: 20
    function: main
  location_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ff99cdf4-0c12-42e5-aa58-30d9da48efe8
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 37
    column: 20
    function: main
  location_invariant:
    string: i <= 999998
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 168b6f0e-215e-49e4-a8ad-4d416b4fb788
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 37
    column: 20
    function: main
  location_invariant:
    string: k <= 999998
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 422f7325-f6a6-45f7-8294-0e2f3b440cf1
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 37
    column: 20
    function: main
  location_invariant:
    string: (-1LL - (long long )k) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 712f2c29-dc39-41dd-babb-fbc86912a9df
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 37
    column: 20
    function: main
  location_invariant:
    string: (0LL - 2LL * (long long )i) + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d7c256a7-d329-411e-81d9-8e20522cbd5b
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 37
    column: 20
    function: main
  location_invariant:
    string: (0LL - (long long )j) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6be8fb75-7e79-43e1-9443-943b5c29ac0b
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 37
    column: 20
    function: main
  location_invariant:
    string: 999999LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 76058c9d-4d4a-4e7d-be17-5ac20c3ebf89
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 37
    column: 20
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 81d3102a-689d-472c-933f-bf729f70f998
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 41
    column: 16
    function: main
  location_invariant:
    string: 1 <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b54c7b32-acb7-46c1-8501-99f8a4416672
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 41
    column: 16
    function: main
  location_invariant:
    string: k <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a9d63701-bc9d-4417-95c4-e9ffbd4fc687
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 41
    column: 16
    function: main
  location_invariant:
    string: n <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a7720a0-f18a-4682-ae5d-e7974329e75a
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 41
    column: 16
    function: main
  location_invariant:
    string: (-1LL - (long long )j) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: abf5a860-f50d-4965-8dd7-a9a71edd2745
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 41
    column: 16
    function: main
  location_invariant:
    string: (0LL - 2LL * (long long )i) + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bb969f88-26ea-4b8d-b6fb-97bf82a97c95
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 41
    column: 16
    function: main
  location_invariant:
    string: 999999LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 00b91ab0-c9b7-4c20-a9fd-ab5d7a039090
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 41
    column: 16
    function: main
  location_invariant:
    string: (long long )k - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 74c80bd6-28b5-4bf2-8167-b39a6bab9f84
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 41
    column: 16
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f35ab60-aa61-431f-9695-2c531616ba19
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 41
    column: 16
    function: main
  location_invariant:
    string: n != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 367035de-f599-4a8b-ab35-1faab9103f4f
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 42
    column: 16
    function: main
  location_invariant:
    string: 1 <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e60d545-43f3-4ec2-b70c-6833e4e74aa8
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 42
    column: 16
    function: main
  location_invariant:
    string: k <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b91843f4-fe3c-43ad-af65-a9fb9a08af1b
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 42
    column: 16
    function: main
  location_invariant:
    string: n <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 24e2d531-65d2-4573-82cb-5003a2edc2ec
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 42
    column: 16
    function: main
  location_invariant:
    string: (-1LL - (long long )j) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3867fd7f-84a9-4cf3-a1ec-9eed250372f3
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 42
    column: 16
    function: main
  location_invariant:
    string: (0LL - 2LL * (long long )i) + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 18fcbfda-2636-4bf5-9207-49aad8553471
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 42
    column: 16
    function: main
  location_invariant:
    string: 999999LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d0fd4b2-6543-4d41-b8cd-433954fcdbfe
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 42
    column: 16
    function: main
  location_invariant:
    string: (long long )k - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e5e5f8d3-86bf-4adb-b53e-8b7f8f119879
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 42
    column: 16
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 69619f67-e2fa-4f28-8cfc-e802e0ac9a2b
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 42
    column: 16
    function: main
  location_invariant:
    string: n != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0fe494f7-0a8b-4923-87cd-850137fc9926
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 47
    column: 2
    function: main
  location_invariant:
    string: 999999LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef2103a9-115f-4493-9219-d64703b59d3f
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 28
    column: 24
    function: main
  location_invariant:
    string: -1000000LL + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9e631ae3-f159-4578-865c-5595c159e927
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 29
    column: 8
    function: main
  location_invariant:
    string: n <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8dd134c7-52c7-448b-a472-ab62b12b85fc
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 29
    column: 8
    function: main
  location_invariant:
    string: 999999LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8b1786ca-e435-408d-baec-68bed99323ab
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 33
    column: 8
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ca5b189c-c671-41d9-92ad-4b3b9ed6d0cc
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 33
    column: 8
    function: main
  loop_invariant:
    string: i <= 999999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c292cb70-683e-4cda-9bf7-290bf388612a
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 33
    column: 8
    function: main
  loop_invariant:
    string: k <= 999999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ae224dc6-4839-48a5-9619-a840f22b8074
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 33
    column: 8
    function: main
  loop_invariant:
    string: n <= 999999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c4f0242-c95d-4740-bdbf-9d9eb05170c0
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 33
    column: 8
    function: main
  loop_invariant:
    string: 999999LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e40da863-58f4-4388-ba91-52ec01bdf62a
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 33
    column: 8
    function: main
  loop_invariant:
    string: (long long )k - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f15d20eb-f980-44f8-ade0-1e8fcc155b05
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 33
    column: 8
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 338f2fb5-66a3-40bc-9893-f7ede447bec4
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 34
    column: 12
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b1ee076d-a42a-440a-8f82-142afbde9d32
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 34
    column: 12
    function: main
  loop_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f48dfb8f-14a7-4441-bea5-8e2bdb01211a
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 34
    column: 12
    function: main
  loop_invariant:
    string: 1 <= n
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 094649d1-a1c9-49db-ac3b-09ad70c91ead
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 34
    column: 12
    function: main
  loop_invariant:
    string: i <= 999998
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f1d722be-f2dd-4df3-8e44-5d346be616ad
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 34
    column: 12
    function: main
  loop_invariant:
    string: j <= 1999996
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bf868685-2492-48bb-b6a7-cc257ff56b99
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 34
    column: 12
    function: main
  loop_invariant:
    string: k <= 999999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 30982da1-f76d-4f8c-9b5e-cdbf8680560f
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 34
    column: 12
    function: main
  loop_invariant:
    string: n <= 999999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 67e7b08b-3741-4e1b-8abe-d25b7440af6f
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 34
    column: 12
    function: main
  loop_invariant:
    string: (-1LL - (long long )i) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bb81b935-5759-42ed-92d3-44dd55e08f9b
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 34
    column: 12
    function: main
  loop_invariant:
    string: (0LL - 2LL * (long long )i) + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 03288373-9e3d-4766-a433-1cd73dc69a9b
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 34
    column: 12
    function: main
  loop_invariant:
    string: (999997LL * (long long )i - 999998LL * (long long )j) + 999998LL * (long
      long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 180bf3ea-d1a3-41ac-9ad3-fc8511737570
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 34
    column: 12
    function: main
  loop_invariant:
    string: 999999LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 503c8774-ed29-4f35-81b8-89ae8c14d443
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 34
    column: 12
    function: main
  loop_invariant:
    string: (long long )k - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 158822a7-3c58-48ae-9e79-82bb59ac44b9
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 34
    column: 12
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 379d24ec-fb57-46e9-acdc-cf4f99d4938e
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 34
    column: 12
    function: main
  loop_invariant:
    string: n != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: afb53c80-2383-4f02-9e93-628d440ef302
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 36
    column: 20
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e73c1ab-1a61-4e67-b5e3-9aa19e02e3ea
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 36
    column: 20
    function: main
  loop_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a22bea9-2f85-408a-9879-70d452f2e6aa
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 36
    column: 20
    function: main
  loop_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 970876f6-33f5-46f5-9a4b-f7df3e0aff9b
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 36
    column: 20
    function: main
  loop_invariant:
    string: 1 <= n
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 532b0ab1-bf63-48c5-a3fa-2af1edc260c9
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 36
    column: 20
    function: main
  loop_invariant:
    string: i <= 999998
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f53af163-f47d-4bd0-98cf-9cc532b0eb34
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 36
    column: 20
    function: main
  loop_invariant:
    string: j <= 999998
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 96b69e0f-547a-4ff4-a356-9fd3d02820e0
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 36
    column: 20
    function: main
  loop_invariant:
    string: k <= 999999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fe0da678-4565-454c-89ee-5de8f40d200f
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 36
    column: 20
    function: main
  loop_invariant:
    string: n <= 999999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3627a5a5-0fe8-40de-92e7-0e3e06859e96
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 36
    column: 20
    function: main
  loop_invariant:
    string: (-1LL - (long long )j) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f632b042-45ce-4097-b5ad-779da5a328f8
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 36
    column: 20
    function: main
  loop_invariant:
    string: (0LL - 2LL * (long long )i) + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a396242-2762-45b0-a59c-331094ff727c
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 36
    column: 20
    function: main
  loop_invariant:
    string: (0LL - (long long )j) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b7fdc94-5e74-4070-8987-e06a14abbe35
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 36
    column: 20
    function: main
  loop_invariant:
    string: (0LL - (long long )k) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5aa83452-d1ff-428c-8537-1597f5a1b6bb
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 36
    column: 20
    function: main
  loop_invariant:
    string: 999999LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5202049f-3d2b-4dfe-9dbe-d51a4150d09f
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 36
    column: 20
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ab17c133-5b9a-4f9d-ab5b-dfa726193ca2
    creation_time: 2023-01-27T16:29:45Z
    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/nested6.i'''
    task:
      input_files:
      - ../plain/nested6.i
      input_file_hashes:
        ../plain/nested6.i: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested6.i
    file_hash: 327b0d5e70f014fe291a4771fe2bbb17cb1148e77fe8f6a261d10a47df8adacc
    line: 36
    column: 20
    function: main
  loop_invariant:
    string: n != 0
    type: assertion
    format: C
