- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 75d77721-3349-46c5-bff4-b7beeb0cadd6
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 25
    column: 6
    function: main
  loop_invariant:
    string: 0 <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1a0db711-c575-4c2d-9c0e-8480e27ff41c
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 25
    column: 6
    function: main
  loop_invariant:
    string: 0 <= b
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 660f0af5-bc33-4f8b-bb88-1c41383073d7
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 25
    column: 6
    function: main
  loop_invariant:
    string: 0 <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 32592070-4ff2-429d-b16a-571ce4b2de0e
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 25
    column: 6
    function: main
  loop_invariant:
    string: a <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 54189900-689d-4ff5-9020-b085ff0755f0
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 25
    column: 6
    function: main
  loop_invariant:
    string: b <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d329991-0100-447d-9941-f1849e267edb
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 25
    column: 6
    function: main
  loop_invariant:
    string: c <= 6
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a9015d3a-ffa7-45a2-bd53-c55bceec00df
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 25
    column: 6
    function: main
  loop_invariant:
    string: -6LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d1b78a8-dbe9-4ec8-82ac-8fd426b0e554
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 25
    column: 6
    function: main
  loop_invariant:
    string: -6LL + (long long )e >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 581b47ac-9fe0-4f9e-9f52-f90f043e5cf2
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 25
    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: e0c13248-b14e-4328-af42-53cf8ad32b39
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 25
    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: fdf8e11f-299f-4b6a-b130-abdb36311947
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 25
    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: c1c7295f-65e2-4b6b-83f6-b7372dfe3d75
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: 0 <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8ae80ac8-c6d2-435d-b20d-2c2f364549eb
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: 0 <= b
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6fee8387-d8ab-4a3e-8a64-0611e5bf3ffe
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: 0 <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 21ae91d1-6a39-4d31-a10a-38ac36ace212
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b20a6ff7-29d0-4545-b3d2-fec0415b1c7b
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: a <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 526b5490-fae1-4490-b56a-90f8ced15512
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: b <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c348eef1-c6d1-491b-b9b9-a7b8c4a4420c
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: c <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d590ac39-c4f4-4591-a673-621d34dc0f8b
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: d <= 6
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a606eb2a-8e64-4818-aa2b-a54868445ad7
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: -6LL + (long long )e >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 32c0867a-5fe0-4910-8cad-8c0e950bda6f
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d70b28c4-330e-4c69-875a-7b090930d088
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ef42af94-d036-4dfa-98f0-99b7978e1a44
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e6fa8f9c-0fc1-4d35-abd4-fd3eefec10b0
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bdfafb57-6958-4474-8f28-fba958224f32
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: 0 <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 41394885-7124-4a4b-b998-9cc66151397b
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: 0 <= b
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 04e2042f-ea56-46d6-bd31-dfe4eee72410
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: 0 <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1cdbbb71-060a-4c4e-819e-9e64294d5a1b
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9fd1dadc-0981-439b-9689-de9ab53e15a4
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: 0 <= e
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ebd4b221-bf84-451e-a483-234508da5c7a
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: a <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c0b633e3-8860-4964-be94-fdb6903fee2f
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: b <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 81f2b6bf-9828-439b-961e-b1582da898d1
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: c <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0587b2c6-1513-4c99-9d44-d2e63a0fb177
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: d <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 175340b6-abf2-4e67-a4f7-a30a362d7c6d
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: e <= 6
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 53164521-e19b-43fc-9fdd-7ed178cbb465
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: 6LL - (long long )e >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c29e0248-3e0b-4394-95e7-7fd2db45993a
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a1b3eb40-2858-4b3a-b221-fd35f64eda0b
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a12bda5-dc0d-4d87-91ca-07990d99813d
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9cac747c-8dbc-4e14-bdb4-b1fc6d1f2d56
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4649afdc-5cc1-4846-a535-d106ade227da
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: (long long )e >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 68420676-d5c9-402d-b764-bf42e65817f3
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 23
    column: 4
    function: main
  loop_invariant:
    string: 0 <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 741cbbc1-2763-4ac3-a2d2-083878bfc40b
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 23
    column: 4
    function: main
  loop_invariant:
    string: a <= 6
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 332dc157-4c14-41d0-a246-09814ea5bcc7
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 23
    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: f6927ce2-27d0-453c-aa21-e08505174285
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 23
    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: 9e90794d-5867-40f1-a384-601aeade71db
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 23
    column: 4
    function: main
  loop_invariant:
    string: -6LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7b6c096e-2a4b-4bcf-a83a-400bae9cc112
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 23
    column: 4
    function: main
  loop_invariant:
    string: -6LL + (long long )e >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 017936c1-8011-4514-96bd-490a4005c820
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 23
    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: d6a65ab9-4413-4be4-9d48-60e5c8570284
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 24
    column: 5
    function: main
  loop_invariant:
    string: 0 <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e21dbbd6-09cf-41e6-a216-1c6f54a20d8c
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 24
    column: 5
    function: main
  loop_invariant:
    string: 0 <= b
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 40747c59-2039-42ec-a3db-81268fffc05b
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 24
    column: 5
    function: main
  loop_invariant:
    string: a <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 87ce1c76-ed3a-49a1-a68d-380232434dc4
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 24
    column: 5
    function: main
  loop_invariant:
    string: b <= 6
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ea1d79f1-41d3-48a4-938e-0a20219924a1
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 24
    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: 3c2f25d5-a099-4493-a753-1a393509d94b
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 24
    column: 5
    function: main
  loop_invariant:
    string: -6LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f14d2435-f36e-4c7a-8d8b-1c7c97059090
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 24
    column: 5
    function: main
  loop_invariant:
    string: -6LL + (long long )e >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 011706d2-458b-47ff-ac2a-af6a1c33ccd9
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 24
    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: 931c588d-cce3-4f39-b5a5-99fdc560946a
    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_5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-simple/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      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_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 24
    column: 5
    function: main
  loop_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
