- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0011861-24d2-4e67-b2ca-532299b696cc
    creation_time: 2023-01-27T16:29:21Z
    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/count_by_k.i'''
    task:
      input_files:
      - ../plain/count_by_k.i
      input_file_hashes:
        ../plain/count_by_k.i: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/count_by_k.i
    file_hash: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
    line: 30
    column: 4
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ce00dfba-8dd0-4b90-913e-13923877e2e5
    creation_time: 2023-01-27T16:29:21Z
    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/count_by_k.i'''
    task:
      input_files:
      - ../plain/count_by_k.i
      input_file_hashes:
        ../plain/count_by_k.i: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/count_by_k.i
    file_hash: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
    line: 30
    column: 4
    function: main
  location_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 008df15a-c655-40f4-9d2e-ffde4c9df2ff
    creation_time: 2023-01-27T16:29:21Z
    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/count_by_k.i'''
    task:
      input_files:
      - ../plain/count_by_k.i
      input_file_hashes:
        ../plain/count_by_k.i: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/count_by_k.i
    file_hash: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
    line: 30
    column: 4
    function: main
  location_invariant:
    string: i <= 10000009
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dde139c0-0513-48c7-8376-a4789e5a74a7
    creation_time: 2023-01-27T16:29:21Z
    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/count_by_k.i'''
    task:
      input_files:
      - ../plain/count_by_k.i
      input_file_hashes:
        ../plain/count_by_k.i: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/count_by_k.i
    file_hash: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
    line: 30
    column: 4
    function: main
  location_invariant:
    string: k <= 10
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d7f090d-ee53-45fb-851e-05f0d482248b
    creation_time: 2023-01-27T16:29:21Z
    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/count_by_k.i'''
    task:
      input_files:
      - ../plain/count_by_k.i
      input_file_hashes:
        ../plain/count_by_k.i: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/count_by_k.i
    file_hash: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
    line: 30
    column: 4
    function: main
  location_invariant:
    string: 10LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a6681300-0d6c-40b0-b522-ab4fcbc5d172
    creation_time: 2023-01-27T16:29:21Z
    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/count_by_k.i'''
    task:
      input_files:
      - ../plain/count_by_k.i
      input_file_hashes:
        ../plain/count_by_k.i: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/count_by_k.i
    file_hash: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
    line: 30
    column: 4
    function: main
  location_invariant:
    string: (long long )i - 1000000LL * (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd97e633-45aa-47c5-978a-c95f69ca303b
    creation_time: 2023-01-27T16:29:21Z
    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/count_by_k.i'''
    task:
      input_files:
      - ../plain/count_by_k.i
      input_file_hashes:
        ../plain/count_by_k.i: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/count_by_k.i
    file_hash: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
    line: 30
    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: d2161eee-1cb8-4898-8475-e2b0593c09de
    creation_time: 2023-01-27T16:29:21Z
    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/count_by_k.i'''
    task:
      input_files:
      - ../plain/count_by_k.i
      input_file_hashes:
        ../plain/count_by_k.i: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/count_by_k.i
    file_hash: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 10LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 075e23c9-69a5-413a-858a-8b38f6424c91
    creation_time: 2023-01-27T16:29:21Z
    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/count_by_k.i'''
    task:
      input_files:
      - ../plain/count_by_k.i
      input_file_hashes:
        ../plain/count_by_k.i: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/count_by_k.i
    file_hash: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (long long )i - 1000000LL * (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f067aafb-59a7-43c4-b6c2-5473ecfa500d
    creation_time: 2023-01-27T16:29:21Z
    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/count_by_k.i'''
    task:
      input_files:
      - ../plain/count_by_k.i
      input_file_hashes:
        ../plain/count_by_k.i: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/count_by_k.i
    file_hash: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
    line: 31
    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: 5446e3ac-9cc5-4cb4-b0fb-877c7f991cdd
    creation_time: 2023-01-27T16:29:21Z
    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/count_by_k.i'''
    task:
      input_files:
      - ../plain/count_by_k.i
      input_file_hashes:
        ../plain/count_by_k.i: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/count_by_k.i
    file_hash: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
    line: 28
    column: 8
    function: main
  location_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f98c1424-8de5-477e-b2d7-bfd2bb61e097
    creation_time: 2023-01-27T16:29:21Z
    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/count_by_k.i'''
    task:
      input_files:
      - ../plain/count_by_k.i
      input_file_hashes:
        ../plain/count_by_k.i: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/count_by_k.i
    file_hash: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
    line: 28
    column: 8
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a173bca4-25b7-47cb-8883-bd50c3404b4f
    creation_time: 2023-01-27T16:29:21Z
    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/count_by_k.i'''
    task:
      input_files:
      - ../plain/count_by_k.i
      input_file_hashes:
        ../plain/count_by_k.i: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/count_by_k.i
    file_hash: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
    line: 28
    column: 30
    function: main
  location_invariant:
    string: -11LL + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 41c8fe14-dd73-42e8-b64b-b75fc27faf59
    creation_time: 2023-01-27T16:29:21Z
    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/count_by_k.i'''
    task:
      input_files:
      - ../plain/count_by_k.i
      input_file_hashes:
        ../plain/count_by_k.i: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/count_by_k.i
    file_hash: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
    line: 28
    column: 30
    function: main
  location_invariant:
    string: -1LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d2bf7acb-6336-458f-85e0-49ad28e69e9d
    creation_time: 2023-01-27T16:29:21Z
    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/count_by_k.i'''
    task:
      input_files:
      - ../plain/count_by_k.i
      input_file_hashes:
        ../plain/count_by_k.i: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/count_by_k.i
    file_hash: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
    line: 29
    column: 8
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d1059ff-55fe-44f4-9878-acad97d79577
    creation_time: 2023-01-27T16:29:21Z
    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/count_by_k.i'''
    task:
      input_files:
      - ../plain/count_by_k.i
      input_file_hashes:
        ../plain/count_by_k.i: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/count_by_k.i
    file_hash: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
    line: 29
    column: 8
    function: main
  loop_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 02762f54-534f-4c56-92bf-70f7c64d44f2
    creation_time: 2023-01-27T16:29:21Z
    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/count_by_k.i'''
    task:
      input_files:
      - ../plain/count_by_k.i
      input_file_hashes:
        ../plain/count_by_k.i: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/count_by_k.i
    file_hash: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
    line: 29
    column: 8
    function: main
  loop_invariant:
    string: i <= 10000009
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c75f921-d2be-4ef2-bf17-afc1408a00f7
    creation_time: 2023-01-27T16:29:21Z
    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/count_by_k.i'''
    task:
      input_files:
      - ../plain/count_by_k.i
      input_file_hashes:
        ../plain/count_by_k.i: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/count_by_k.i
    file_hash: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
    line: 29
    column: 8
    function: main
  loop_invariant:
    string: k <= 10
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: abaebf83-9074-483e-9c9b-996fddf96ca1
    creation_time: 2023-01-27T16:29:21Z
    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/count_by_k.i'''
    task:
      input_files:
      - ../plain/count_by_k.i
      input_file_hashes:
        ../plain/count_by_k.i: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/count_by_k.i
    file_hash: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
    line: 29
    column: 8
    function: main
  loop_invariant:
    string: 10LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5cad550a-32a4-404c-a767-ff0b42fab953
    creation_time: 2023-01-27T16:29:21Z
    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/count_by_k.i'''
    task:
      input_files:
      - ../plain/count_by_k.i
      input_file_hashes:
        ../plain/count_by_k.i: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/count_by_k.i
    file_hash: ee41851a84d57c0c483c2a5edf48180b7c141c1991cdc82f0d66c6775eb49f5b
    line: 29
    column: 8
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
