- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 45972010-df8d-405f-b25c-86534e00da55
    creation_time: 2023-01-27T15:24:34Z
    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-simple/nested_3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
      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-simple/nested_3.c
    file_hash: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
    line: 23
    column: 6
    function: main
  loop_invariant:
    string: 0 <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 83bf6e06-6cb5-425a-aff8-841663b0da41
    creation_time: 2023-01-27T15:24:34Z
    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-simple/nested_3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
      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-simple/nested_3.c
    file_hash: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
    line: 23
    column: 6
    function: main
  loop_invariant:
    string: 0 <= b
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 27b0dc34-c791-44b9-9d24-4c2a53136d09
    creation_time: 2023-01-27T15:24:34Z
    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-simple/nested_3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
      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-simple/nested_3.c
    file_hash: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
    line: 23
    column: 6
    function: main
  loop_invariant:
    string: 0 <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a190998-633b-44a1-90cd-5312d1057d5f
    creation_time: 2023-01-27T15:24:34Z
    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-simple/nested_3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
      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-simple/nested_3.c
    file_hash: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
    line: 23
    column: 6
    function: main
  loop_invariant:
    string: a <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 05656fc4-5c19-4bef-aaec-2f47032b5fa6
    creation_time: 2023-01-27T15:24:34Z
    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-simple/nested_3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
      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-simple/nested_3.c
    file_hash: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
    line: 23
    column: 6
    function: main
  loop_invariant:
    string: b <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6777fe8b-ba1a-4600-b683-285faa1b7630
    creation_time: 2023-01-27T15:24:34Z
    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-simple/nested_3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
      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-simple/nested_3.c
    file_hash: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
    line: 23
    column: 6
    function: main
  loop_invariant:
    string: c <= 6
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 64ee33e5-7cca-4e11-9842-3673f0c080cf
    creation_time: 2023-01-27T15:24:34Z
    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-simple/nested_3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
      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-simple/nested_3.c
    file_hash: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
    line: 23
    column: 6
    function: main
  loop_invariant:
    string: 6LL - (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f7f9242d-c205-475e-a86b-a355df2d8b52
    creation_time: 2023-01-27T15:24:34Z
    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-simple/nested_3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
      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-simple/nested_3.c
    file_hash: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
    line: 23
    column: 6
    function: main
  loop_invariant:
    string: (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5ad2bd06-bb38-4634-854f-daa17f3bf8f4
    creation_time: 2023-01-27T15:24:34Z
    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-simple/nested_3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
      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-simple/nested_3.c
    file_hash: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
    line: 23
    column: 6
    function: main
  loop_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8b7fb884-98f7-4515-8188-e951775b233c
    creation_time: 2023-01-27T15:24:34Z
    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-simple/nested_3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
      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-simple/nested_3.c
    file_hash: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
    line: 23
    column: 6
    function: main
  loop_invariant:
    string: (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8f27eefc-4008-4b7a-adf2-dfba9e1340d6
    creation_time: 2023-01-27T15:24:34Z
    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-simple/nested_3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
      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-simple/nested_3.c
    file_hash: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
    line: 21
    column: 4
    function: main
  loop_invariant:
    string: 0 <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b93df767-568c-4ed1-b816-a14ed1283800
    creation_time: 2023-01-27T15:24:34Z
    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-simple/nested_3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
      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-simple/nested_3.c
    file_hash: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
    line: 21
    column: 4
    function: main
  loop_invariant:
    string: a <= 6
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 05f03773-5ae9-4932-9e75-4f25a5e64332
    creation_time: 2023-01-27T15:24:34Z
    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-simple/nested_3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
      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-simple/nested_3.c
    file_hash: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
    line: 21
    column: 4
    function: main
  loop_invariant:
    string: -6LL + (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b77fc835-c1b6-4ee4-b4e6-5181beb6c1e8
    creation_time: 2023-01-27T15:24:34Z
    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-simple/nested_3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
      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-simple/nested_3.c
    file_hash: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
    line: 21
    column: 4
    function: main
  loop_invariant:
    string: -6LL + (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ce6bd6ec-35f9-45af-8688-8c3e20e01adf
    creation_time: 2023-01-27T15:24:34Z
    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-simple/nested_3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
      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-simple/nested_3.c
    file_hash: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
    line: 21
    column: 4
    function: main
  loop_invariant:
    string: (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fc59d05c-dcd1-467e-b085-27618b14a71d
    creation_time: 2023-01-27T15:24:34Z
    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-simple/nested_3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
      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-simple/nested_3.c
    file_hash: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
    line: 22
    column: 5
    function: main
  loop_invariant:
    string: 0 <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 84b3d817-e208-4317-91c4-30c69cfb2bcf
    creation_time: 2023-01-27T15:24:34Z
    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-simple/nested_3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
      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-simple/nested_3.c
    file_hash: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
    line: 22
    column: 5
    function: main
  loop_invariant:
    string: 0 <= b
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a7c4ebab-bac1-4084-8698-c2310762cea0
    creation_time: 2023-01-27T15:24:34Z
    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-simple/nested_3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
      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-simple/nested_3.c
    file_hash: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
    line: 22
    column: 5
    function: main
  loop_invariant:
    string: a <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1afa472b-b23d-4fbd-82c5-8c88547db3f7
    creation_time: 2023-01-27T15:24:34Z
    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-simple/nested_3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
      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-simple/nested_3.c
    file_hash: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
    line: 22
    column: 5
    function: main
  loop_invariant:
    string: b <= 6
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 950472d4-3a01-4a6b-8410-91a0668d70b3
    creation_time: 2023-01-27T15:24:34Z
    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-simple/nested_3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
      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-simple/nested_3.c
    file_hash: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
    line: 22
    column: 5
    function: main
  loop_invariant:
    string: -6LL + (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 47680854-04ce-4401-a7be-e2f0ffe76f5c
    creation_time: 2023-01-27T15:24:34Z
    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-simple/nested_3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
      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-simple/nested_3.c
    file_hash: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
    line: 22
    column: 5
    function: main
  loop_invariant:
    string: (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b0618ed-9ad8-4cc8-b4ce-b123243bb861
    creation_time: 2023-01-27T15:24:34Z
    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-simple/nested_3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_3.c: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
      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-simple/nested_3.c
    file_hash: 6a30debb45adf4eb2040807436dec0136066a492a6c11eb0dbebd1f179f328d9
    line: 22
    column: 5
    function: main
  loop_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
