- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c5f62f3f-d38a-434b-8fd9-96b4d54835cb
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark34_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark34_conjunctive.i
      input_file_hashes:
        ../plain/benchmark34_conjunctive.i: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark34_conjunctive.i
    file_hash: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a9a8abf8-4db2-4078-9406-300d3b4ed021
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark34_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark34_conjunctive.i
      input_file_hashes:
        ../plain/benchmark34_conjunctive.i: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark34_conjunctive.i
    file_hash: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
    line: 25
    column: 4
    function: main
  location_invariant:
    string: j <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8a906118-0208-47d6-b0dc-9d8adcbbe966
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark34_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark34_conjunctive.i
      input_file_hashes:
        ../plain/benchmark34_conjunctive.i: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark34_conjunctive.i
    file_hash: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
    line: 25
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cabf8f57-3fb4-4f1b-a5b7-406acfb10f8a
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark34_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark34_conjunctive.i
      input_file_hashes:
        ../plain/benchmark34_conjunctive.i: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark34_conjunctive.i
    file_hash: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
    line: 25
    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: fd8105db-c87a-4e41-8983-d6bba6e9d2a9
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark34_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark34_conjunctive.i
      input_file_hashes:
        ../plain/benchmark34_conjunctive.i: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark34_conjunctive.i
    file_hash: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
    line: 25
    column: 8
    function: main
  location_invariant:
    string: 1 <= j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a362489-082e-4438-920d-97c87f988d4d
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark34_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark34_conjunctive.i
      input_file_hashes:
        ../plain/benchmark34_conjunctive.i: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark34_conjunctive.i
    file_hash: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
    line: 25
    column: 8
    function: main
  location_invariant:
    string: 1 <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0f8bfcf5-f349-46fc-9c92-b7b698cc6851
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark34_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark34_conjunctive.i
      input_file_hashes:
        ../plain/benchmark34_conjunctive.i: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark34_conjunctive.i
    file_hash: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
    line: 25
    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: c045035e-12b0-48c8-91f1-aa4863720753
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark34_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark34_conjunctive.i
      input_file_hashes:
        ../plain/benchmark34_conjunctive.i: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark34_conjunctive.i
    file_hash: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
    line: 25
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: afe8ccf2-7392-4a92-9a22-bfae823518a7
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark34_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark34_conjunctive.i
      input_file_hashes:
        ../plain/benchmark34_conjunctive.i: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark34_conjunctive.i
    file_hash: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
    line: 25
    column: 8
    function: main
  location_invariant:
    string: n != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 675ad3a6-8ce5-4552-aa98-cc0594cbe939
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark34_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark34_conjunctive.i
      input_file_hashes:
        ../plain/benchmark34_conjunctive.i: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark34_conjunctive.i
    file_hash: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
    line: 27
    column: 2
    function: main
  location_invariant:
    string: (-1LL + (long long )j) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7150781f-433f-4937-9dfc-2a6ec83c9aec
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark34_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark34_conjunctive.i
      input_file_hashes:
        ../plain/benchmark34_conjunctive.i: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark34_conjunctive.i
    file_hash: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
    line: 27
    column: 2
    function: main
  location_invariant:
    string: 0LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a8a0eaa8-09af-43d5-b3e1-c4dde2df014b
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark34_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark34_conjunctive.i
      input_file_hashes:
        ../plain/benchmark34_conjunctive.i: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark34_conjunctive.i
    file_hash: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
    line: 28
    column: 2
    function: main
  location_invariant:
    string: (-1LL + (long long )j) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 34f6b407-d9ae-4f67-9afa-7917ce0588ba
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark34_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark34_conjunctive.i
      input_file_hashes:
        ../plain/benchmark34_conjunctive.i: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark34_conjunctive.i
    file_hash: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
    line: 28
    column: 2
    function: main
  location_invariant:
    string: 0LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f7e172d3-470b-402c-a9ef-4d60ce6641ca
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark34_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark34_conjunctive.i
      input_file_hashes:
        ../plain/benchmark34_conjunctive.i: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark34_conjunctive.i
    file_hash: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
    line: 23
    column: 36
    function: main
  location_invariant:
    string: 0LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d11267f7-2781-41fb-bf2a-d310f270b50c
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark34_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark34_conjunctive.i
      input_file_hashes:
        ../plain/benchmark34_conjunctive.i: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark34_conjunctive.i
    file_hash: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
    line: 24
    column: 9
    function: main
  loop_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0929992b-234e-40eb-bf0f-bcf63eb6e43d
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark34_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark34_conjunctive.i
      input_file_hashes:
        ../plain/benchmark34_conjunctive.i: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark34_conjunctive.i
    file_hash: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
    line: 24
    column: 9
    function: main
  loop_invariant:
    string: 1 <= n
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5b70690c-59a6-4b50-ab50-d6027cc3f915
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark34_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark34_conjunctive.i
      input_file_hashes:
        ../plain/benchmark34_conjunctive.i: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark34_conjunctive.i
    file_hash: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
    line: 24
    column: 9
    function: main
  loop_invariant:
    string: (-1LL + (long long )j) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a277c79e-9434-489a-909c-66767a913e34
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark34_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark34_conjunctive.i
      input_file_hashes:
        ../plain/benchmark34_conjunctive.i: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark34_conjunctive.i
    file_hash: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
    line: 24
    column: 9
    function: main
  loop_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c5901f76-0865-42c7-a1ca-59c45dec3221
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark34_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark34_conjunctive.i
      input_file_hashes:
        ../plain/benchmark34_conjunctive.i: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark34_conjunctive.i
    file_hash: 0414607cdfaf86248673acc731020b311087823754eb03e229e19e48245fa120
    line: 24
    column: 9
    function: main
  loop_invariant:
    string: n != 0
    type: assertion
    format: C
