- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 159e2a65-336b-4b52-8776-9443c5df56b2
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dd8bf88b-f09d-4795-8432-f94f432e7166
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 32
    column: 4
    function: main
  location_invariant:
    string: i <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 96c1e396-fe0d-4b3a-aead-ffb9e439767e
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 1000000LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f9ceb92b-3380-42a5-882f-2881c3039a18
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f636a703-a7a9-431b-b5e1-c03fa7d85280
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 34
    column: 6
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5542220f-d77d-48db-9d47-919382859107
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 34
    column: 6
    function: main
  location_invariant:
    string: i <= 1000001
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b5fb70d-0a78-4685-957b-a1f5ff9a9c11
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 34
    column: 6
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e556c6fb-dfa4-4b6a-859d-74a57c26fcda
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 35
    column: 4
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 83ea0f13-2131-4af5-bd7a-34c088cea95a
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 35
    column: 4
    function: main
  location_invariant:
    string: i <= 1000001
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e54eac1c-c77b-43d7-b345-13f6a6473a52
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 35
    column: 4
    function: main
  location_invariant:
    string: pvlen <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 08cb5027-ce71-4b4b-95e8-0e6a7512a2c9
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 35
    column: 4
    function: main
  location_invariant:
    string: (-1LL + (long long )i) - (long long )pvlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 671e86cd-758d-4b60-804d-12260d71de34
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 35
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6693e29b-4f55-4da4-8b3c-71cebecf7066
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 37
    column: 2
    function: main
  location_invariant:
    string: 0 <= pvlen
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2ed36170-55d4-4428-aa8d-a42282ae12fb
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 37
    column: 2
    function: main
  location_invariant:
    string: (0LL - (long long )i) + (long long )pvlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e7a915a5-1d90-4fb4-9250-59823e385da1
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 37
    column: 2
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a8918bef-f555-421d-b9a8-3c01edeb3827
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 39
    column: 4
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f94271b-a2ce-45fc-8915-03d26a94fb7c
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 39
    column: 4
    function: main
  location_invariant:
    string: i <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ab288f75-28fe-475c-b1f1-2e414dadb01e
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 39
    column: 4
    function: main
  location_invariant:
    string: 1000000LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cf8bfe4c-7387-4e03-82ed-c956b997c699
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 39
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd501944-f492-4f5b-a2d0-08f81573cbdc
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 39
    column: 4
    function: main
  location_invariant:
    string: (long long )pvlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f449b904-7191-4173-a263-a3aff7a0bd90
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 40
    column: 4
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6b6c40da-5ffd-4030-b7de-648a1d4fb6b6
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 40
    column: 4
    function: main
  location_invariant:
    string: i <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af45293f-0ab5-4e7b-85ef-e02d23749e9f
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 40
    column: 4
    function: main
  location_invariant:
    string: 1000000LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a10df30-78e4-4116-b365-6f3ab0feb0b3
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 40
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e4f15031-e1d2-4289-b900-2c246f7856b4
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 40
    column: 4
    function: main
  location_invariant:
    string: (long long )pvlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b64341af-6ea9-4a01-9145-ece30e4142b7
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 41
    column: 4
    function: main
  location_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d6e1ef2-3f0f-4605-aa19-ce81508fd41e
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 41
    column: 4
    function: main
  location_invariant:
    string: 1 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b256584-0e0f-43d2-8a75-00fd48f9869a
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 41
    column: 4
    function: main
  location_invariant:
    string: i <= 1000001
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 57df5215-6e27-4483-affb-e3d03c8eea41
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 41
    column: 4
    function: main
  location_invariant:
    string: k <= 1000001
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 672bcbb5-8366-4032-9465-ae601e070d4a
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 41
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a004d03f-e6e3-4f7b-94b1-db87169ff34b
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 41
    column: 4
    function: main
  location_invariant:
    string: 1000001LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43fe5dd2-b4d2-4911-add2-4cba3c8d949f
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 41
    column: 4
    function: main
  location_invariant:
    string: (long long )pvlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b723a347-ce1b-401d-8d1e-748e361d3107
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 43
    column: 6
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 75646d4b-2f1a-4afd-88fd-ef0899748ce8
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 43
    column: 6
    function: main
  location_invariant:
    string: (long long )pvlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 00ab2a8f-5737-4424-b7d3-96b6abe273f0
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 44
    column: 2
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d633b48f-0c9e-434a-a984-9253d426b9d2
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 44
    column: 2
    function: main
  location_invariant:
    string: i <= 1000001
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c78d6b4a-7379-4d48-a12b-d073c01ce3cd
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 44
    column: 2
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 55ba293c-3e6d-48e2-b4cd-a09222dc815b
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 44
    column: 2
    function: main
  location_invariant:
    string: (long long )pvlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cac4e33c-32b2-4c1e-aa44-1c04676d1bd1
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 46
    column: 4
    function: main
  location_invariant:
    string: k <= 1000001
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 77e6a58c-d294-47df-a92a-fec43a7eebda
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 46
    column: 4
    function: main
  location_invariant:
    string: (long long )pvlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0b1491ad-2e91-48c7-88bc-e59af19dc9f5
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 46
    column: 4
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14f5140e-1a98-4200-b8be-79cf9a314c20
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 47
    column: 4
    function: main
  location_invariant:
    string: k <= 1000001
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 03d1099d-423e-4f51-ba45-c6ed675d0660
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 47
    column: 4
    function: main
  location_invariant:
    string: (long long )pvlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8ef1a4ac-8845-4357-b55c-e17904bec829
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 47
    column: 4
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f5bf3e20-f4fd-4435-8530-a226dd90844f
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 48
    column: 4
    function: main
  location_invariant:
    string: i <= 1000001
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 377c930c-3edd-45cb-bfa5-2b96d6e03c2b
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 48
    column: 4
    function: main
  location_invariant:
    string: k <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b20e8ca9-202f-4d0b-92b3-2323910c56c4
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 48
    column: 4
    function: main
  location_invariant:
    string: (long long )pvlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 96837860-688e-4766-9445-68757e96b168
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 48
    column: 4
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 98da5b2b-0f77-4695-9310-dfd667a280c3
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 49
    column: 4
    function: main
  location_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d5247fb0-2357-48b7-bdcc-615cc34e98d5
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 49
    column: 4
    function: main
  location_invariant:
    string: i <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3710d584-92d3-40eb-ae1e-fc0d6b2008b8
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 49
    column: 4
    function: main
  location_invariant:
    string: j <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9363c4f0-aa24-49cf-aefa-c25397c95fcc
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 49
    column: 4
    function: main
  location_invariant:
    string: (long long )pvlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5520d8c9-2824-49c5-a5de-a8e34d5578b1
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 49
    column: 4
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 62955328-c6b6-44ac-a2ad-5463adc580de
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 50
    column: 8
    function: main
  location_invariant:
    string: 0 <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 445ad83d-63a1-4978-bc6b-58ff149dad91
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 50
    column: 8
    function: main
  location_invariant:
    string: 1 <= j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 61836df7-187d-4be7-bd53-f9eaa9f2e612
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 50
    column: 8
    function: main
  location_invariant:
    string: i <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cf51ba55-4eb2-4558-af38-ff6bf5dc4896
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 50
    column: 8
    function: main
  location_invariant:
    string: n <= 1000001
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b1c6f452-84f3-42f2-bb5d-48068ccfa15b
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 50
    column: 8
    function: main
  location_invariant:
    string: j <= 1000001
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb4f66c8-8866-4135-bd6e-8c3c5d3f8cb6
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 50
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 038c9a8a-a4ca-44c4-88d6-956e15f7e670
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 50
    column: 8
    function: main
  location_invariant:
    string: (long long )pvlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4603b1f0-7d2f-45e6-b72f-03b82ea78eea
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 54
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cda1a6fd-1541-40f3-9a37-79f9be190162
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 54
    column: 2
    function: main
  location_invariant:
    string: 0LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 677646b3-fcde-482d-8449-759acfc8b4c1
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 54
    column: 2
    function: main
  location_invariant:
    string: (long long )pvlen >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 89b6bb8e-ef18-4f29-b863-9cd5ab9d7b3d
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 31
    column: 10
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 06f1662d-161d-4785-b336-bbae1b52cc3b
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 31
    column: 10
    function: main
  loop_invariant:
    string: i <= 1000001
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: de106124-ef3b-4bf0-910f-23a6eb322ca7
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 31
    column: 10
    function: main
  loop_invariant:
    string: 1000001LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5cf46128-1c2e-42e9-a3d1-28e4d9f5a441
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 31
    column: 10
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 663c7e2c-f058-4d4c-904e-40592d564755
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ac2850c2-fa39-4ea2-945a-273ad544452b
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: 0 <= pvlen
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ae113149-3f22-49b9-9c5d-a552c0db6a62
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ec9a886-9531-47ed-bfec-b2f04bb2a98c
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: i <= 1000001
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 113f22c0-8e90-4421-b21f-3f923eca40d6
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: k <= 1000001
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f2486f49-0aa3-4a26-8c54-a7d09042f93b
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: 1000001LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1eb86f25-395d-425b-b139-cedf1d0909ef
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d90bb92d-1869-4df7-865d-d66d06c59c12
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: (long long )pvlen >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c1c43e4-274e-42e5-bc75-dd7079f71bfc
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 45
    column: 9
    function: main
  loop_invariant:
    string: 0 <= pvlen
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3b7387b7-b8e4-4e7e-88a5-5494d8e525f3
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 45
    column: 9
    function: main
  loop_invariant:
    string: 0 <= n
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f280a842-5b50-43b8-a760-b90cf9343380
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 45
    column: 9
    function: main
  loop_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: aa12752c-39c8-488d-9a58-e36881fd13e6
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 45
    column: 9
    function: main
  loop_invariant:
    string: i <= 1000001
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9c64a1e3-b2a9-44cd-8693-84920e133549
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 45
    column: 9
    function: main
  loop_invariant:
    string: k <= 1000001
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b4005226-4bdb-4ae4-9a75-0e3a1eb2ea68
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 45
    column: 9
    function: main
  loop_invariant:
    string: n <= 1000001
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 03dcfbf9-b174-41d6-8214-01d4c18f2f06
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 45
    column: 9
    function: main
  loop_invariant:
    string: j <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 343b6ffd-0118-43ef-a1d7-230fe41eeaae
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 45
    column: 9
    function: main
  loop_invariant:
    string: (long long )pvlen >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1c3cea3e-8b4b-4262-8faf-f797f1fb0935
    creation_time: 2023-01-27T16:29:30Z
    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/fragtest_simple.i'''
    task:
      input_files:
      - ../plain/fragtest_simple.i
      input_file_hashes:
        ../plain/fragtest_simple.i: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fragtest_simple.i
    file_hash: be3b53cc5f9badbf5402cafcfa5766831674eb009261bc7c1bcbe9580aece38e
    line: 45
    column: 9
    function: main
  loop_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
