- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 094cc582-8273-4253-b910-4abe7a0d5014
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 35
    column: 8
    function: main
  loop_invariant:
    string: 0 <= r
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 16ff6523-23e0-4aa0-84de-3c9784b78cde
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 35
    column: 8
    function: main
  loop_invariant:
    string: 1 <= n
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bd84010e-9777-4ef9-8cb7-9c19d3665be8
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 35
    column: 8
    function: main
  loop_invariant:
    string: 1 <= l
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: db763844-4611-4f7c-afd1-cd949b43b941
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 35
    column: 8
    function: main
  loop_invariant:
    string: n <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 574d7ac3-7aa6-439c-9093-769b745ae7b1
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 35
    column: 8
    function: main
  loop_invariant:
    string: l <= 500000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bdbe6fbc-8bdb-4b51-9cb2-b8c7fc169984
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 35
    column: 8
    function: main
  loop_invariant:
    string: r <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7860b24b-464f-4565-b308-85524d75d400
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 35
    column: 8
    function: main
  loop_invariant:
    string: -1LL + (long long )l >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 768842bc-5b01-4b40-9cb8-b59d6445a3c1
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 35
    column: 8
    function: main
  loop_invariant:
    string: ((0LL - 2LL * (long long )l) + 2LL * (long long )n) - (long long )r >=
      0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 26b99f74-84be-4738-a93f-7bb9d31f1966
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 35
    column: 8
    function: main
  loop_invariant:
    string: (long long )n - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 22790603-99c0-423b-8895-b19827c10dbe
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 35
    column: 8
    function: main
  loop_invariant:
    string: n != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4611b191-7696-4137-a386-f0ff629febf3
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: 1 <= n
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fcfdfd40-41e3-430b-959c-25082dc61311
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: 1 <= l
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a18343b6-8392-4ced-9924-8c048d3cdf2b
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: 1 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7785707f-1fba-44bb-b713-9e538b1cf24c
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: 2 <= r
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c389769-ffb0-46df-8755-8cd6dabe7815
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: 2 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 78b303ec-f3ac-4497-a32c-37d0090c93d9
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: n <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ba7c0cf7-9c8c-45f0-9e28-4ffd82079ee7
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: l <= 500000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5b54243d-444d-47bc-9749-684ee99ad62d
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: r <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 90999e4a-df44-4604-a93c-488589d1be4e
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: i <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 04e533f6-092f-49ab-8e5e-357ae7bd60f1
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: j <= 2000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1cc6fc86-d157-4aa8-9f94-62697d4ddf98
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: -2LL + (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c2269909-2a9a-4a12-887a-9d8b8fd6cefd
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: -1LL + (long long )l >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 77d7f70b-beef-4df8-8a38-b20f56150b94
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: ((-1LL - (long long )i) + (long long )l) + (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 426bc00b-d8b6-491e-a069-d9c2d6a41b15
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: (0LL - (long long )i) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 45b3a5fd-b858-45ea-adf2-e24ec76466d6
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: ((0LL - 2LL * (long long )l) + 2LL * (long long )n) - (long long )r >=
      0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 25873266-e4e4-43d2-905f-bb7439f4eefc
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: (long long )n - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c4a4a91a-baa9-4c0c-adfe-8e6b9e6e0557
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: (long long )i - (long long )l >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8e1568af-c325-4808-9853-e900fda41777
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: n != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1352a2b5-1b45-48c2-a507-584a224dd383
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: r != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a32d0293-4a05-471b-b214-ffb2f2aa6725
    creation_time: 2023-01-27T15:24:22Z
    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/loop-invgen/heapsort.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/heapsort.i
    file_hash: 8e7c8e5dc2a9e8f11b25d1bb9948f05f37b9553e3dc9f8bd8213088dea43cb37
    line: 38
    column: 10
    function: main
  loop_invariant:
    string: i != 0
    type: assertion
    format: C
