- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5db99be1-b168-4f85-ab8f-e86eaf0ca6b5
    creation_time: 2023-01-27T15:24:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 30
    column: 5
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f53bfce9-e8bb-4748-9614-4c5593ea47c1
    creation_time: 2023-01-27T15:24:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 30
    column: 5
    function: main
  loop_invariant:
    string: (long long )M - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9717a885-f3db-46ce-b67d-16bb86944db7
    creation_time: 2023-01-27T15:24:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 30
    column: 5
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ae61693-9fbf-4914-a642-5fe5494bae10
    creation_time: 2023-01-27T15:24:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 34
    column: 5
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a0af217b-08ae-4325-9518-718d4d04934b
    creation_time: 2023-01-27T15:24:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 34
    column: 5
    function: main
  loop_invariant:
    string: (long long )M - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 25d8448d-9a6d-490a-a086-ec138edd20bf
    creation_time: 2023-01-27T15:24:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 34
    column: 5
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d241e19-7fdd-4f4e-a2e0-ef75187495dd
    creation_time: 2023-01-27T15:24:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 38
    column: 5
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b5a5502e-2c85-4ec0-bd53-18d601b24cc6
    creation_time: 2023-01-27T15:24:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 38
    column: 5
    function: main
  loop_invariant:
    string: (long long )M - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 54399e8f-2d7f-42dc-aea5-88796652eb83
    creation_time: 2023-01-27T15:24:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 38
    column: 5
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5609203c-2f5f-4144-b89d-560c71ee8cbc
    creation_time: 2023-01-27T15:24:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 40
    column: 5
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )M >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 008161ba-e337-47df-97a6-92dc0b775feb
    creation_time: 2023-01-27T15:24:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 40
    column: 5
    function: main
  loop_invariant:
    string: (long long )M - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ee04fb0b-8aad-4a1d-b52a-568535f9bb43
    creation_time: 2023-01-27T15:24:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/sum_array-2.i
    file_hash: 84226515a723f10f2a919f265c45890771224ac18b5dd5f986441c53175929f5
    line: 40
    column: 5
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
