- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 28076152-82a9-47ae-8bc6-9f5fe19272b8
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 32
    column: 9
    function: main
  loop_invariant:
    string: -1000000 <= n0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 02cb93de-3a14-4132-8746-94e1a7cefa5c
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 32
    column: 9
    function: main
  loop_invariant:
    string: -1000000 <= n1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 065aa8f0-b023-4ab5-8f30-47c5af730cc8
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 32
    column: 9
    function: main
  loop_invariant:
    string: 0 <= i0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5f40b96e-63f6-4328-9d1f-1cecc6b6be33
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 32
    column: 9
    function: main
  loop_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e5d4e26-597e-4564-814d-1cf106dce515
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 32
    column: 9
    function: main
  loop_invariant:
    string: n0 <= 999999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 095c8385-d960-4a16-8638-f532e1e0e0b9
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 32
    column: 9
    function: main
  loop_invariant:
    string: n1 <= 999999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 31c87dbd-6440-4ad0-b965-7aca18c7200f
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 32
    column: 9
    function: main
  loop_invariant:
    string: i0 <= 999999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 87141d1d-2837-4cc9-8330-4cdfc822517f
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 32
    column: 9
    function: main
  loop_invariant:
    string: k <= 999999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f3d87e7-074f-42c3-9883-17295e71add9
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 32
    column: 9
    function: main
  loop_invariant:
    string: 1000000LL + (long long )n1 >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f00ce2d4-3d16-4cbe-a065-0a28d1a4e4b6
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 32
    column: 9
    function: main
  loop_invariant:
    string: 999999LL - (long long )n0 >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 899f39b4-bded-413b-bc24-e3cf20894662
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 32
    column: 9
    function: main
  loop_invariant:
    string: 999999LL - (long long )n1 >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 141dc75a-de2c-4830-96a0-00591988b099
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 32
    column: 9
    function: main
  loop_invariant:
    string: (long long )i0 >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e584c1f7-0292-45ee-91aa-d4c50d49ae75
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 37
    column: 9
    function: main
  loop_invariant:
    string: -1000000 <= n0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 28698274-c540-48cf-ab58-7ea0e0bfe590
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 37
    column: 9
    function: main
  loop_invariant:
    string: -1000000 <= n1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 91bfd606-a17d-4a0d-bf27-6bbc4acee091
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 37
    column: 9
    function: main
  loop_invariant:
    string: 0 <= i0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e636991c-6660-4838-8d8b-32bd6ce61ee7
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 37
    column: 9
    function: main
  loop_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e512a809-799a-4ac9-88f5-e26805c4c0da
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 37
    column: 9
    function: main
  loop_invariant:
    string: 0 <= i1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 692a7bcc-8107-4026-9144-a709b9c78028
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 37
    column: 9
    function: main
  loop_invariant:
    string: n0 <= 999999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 40ae5ff8-acf8-4cbf-9833-decb73f7228d
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 37
    column: 9
    function: main
  loop_invariant:
    string: n1 <= 999999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 42b3911e-71d1-4e43-8049-580eb7ef51ba
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 37
    column: 9
    function: main
  loop_invariant:
    string: i0 <= 999999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c69dc663-fdec-42b4-8a06-883bf80fb201
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 37
    column: 9
    function: main
  loop_invariant:
    string: i1 <= 999999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7931849a-f486-4941-b58a-43f9abbb10cf
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 37
    column: 9
    function: main
  loop_invariant:
    string: 999999LL - (long long )n0 >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c04d23b-f1d4-4c44-8019-9b220f6b249f
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 37
    column: 9
    function: main
  loop_invariant:
    string: 999999LL - (long long )n1 >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bd5f7866-2d0d-45b2-912c-dcfa51f0c52e
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 37
    column: 9
    function: main
  loop_invariant:
    string: (long long )i0 - (long long )n0 >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: be91e4a0-73a0-4ed2-b805-7773149eb304
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 37
    column: 9
    function: main
  loop_invariant:
    string: (long long )i0 >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bc4c3d55-540f-4530-8e98-3c009426ee48
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 37
    column: 9
    function: main
  loop_invariant:
    string: (long long )i1 >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 46f1a3c6-0327-46a1-b088-1f57736e3fdf
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 42
    column: 9
    function: main
  loop_invariant:
    string: -1000000 <= n0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b1149b95-aa1e-4b67-b2ea-69b78f07d886
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 42
    column: 9
    function: main
  loop_invariant:
    string: -1000000 <= n1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ef95ef8-85d9-4969-9e35-7c5bd262a937
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 42
    column: 9
    function: main
  loop_invariant:
    string: 0 <= i0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 674d66bb-0c71-4c19-bd61-eb72a0d339df
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 42
    column: 9
    function: main
  loop_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 24e263d7-02b6-4ae3-aebc-f8d7bc66b4ce
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 42
    column: 9
    function: main
  loop_invariant:
    string: 0 <= i1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8ba2a22e-4a2a-4406-af5b-976d904ca195
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 42
    column: 9
    function: main
  loop_invariant:
    string: 0 <= j1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 577abed4-e52a-4221-ab8e-6a8e34db5b42
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 42
    column: 9
    function: main
  loop_invariant:
    string: n0 <= 999999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 77e3ecee-0570-49d9-8bc3-b98df9d4e52e
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 42
    column: 9
    function: main
  loop_invariant:
    string: n1 <= 999999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 82e6eaf2-266c-4db2-bbb2-b54c876c3001
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 42
    column: 9
    function: main
  loop_invariant:
    string: i0 <= 999999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4cc9b11e-c106-4a89-b412-e88c75891da5
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 42
    column: 9
    function: main
  loop_invariant:
    string: i1 <= 999999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ed2b946b-3673-410e-989b-f2e5501fb905
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 42
    column: 9
    function: main
  loop_invariant:
    string: j1 <= 1999998
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f6bf4c68-a6c9-45e7-a4d2-4959ce05ac6f
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 42
    column: 9
    function: main
  loop_invariant:
    string: 999999LL - (long long )n0 >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 60aab4e7-24dd-4352-a4d0-94cf1d725abb
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 42
    column: 9
    function: main
  loop_invariant:
    string: 999999LL - (long long )n1 >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bd3bb163-69c6-4354-873b-ec1d961c3231
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 42
    column: 9
    function: main
  loop_invariant:
    string: (long long )i0 - (long long )n0 >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4f7c7427-f35b-44f9-9b87-571853897a66
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 42
    column: 9
    function: main
  loop_invariant:
    string: (long long )i1 - (long long )n1 >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5ae3981e-cc67-4f12-b87e-ff68cf4e3144
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 42
    column: 9
    function: main
  loop_invariant:
    string: (long long )i0 >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b9475221-76be-437c-b191-0a6e2b3f9ce6
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 42
    column: 9
    function: main
  loop_invariant:
    string: (long long )i1 >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 04805fc3-a577-4d9c-9134-346907259c10
    creation_time: 2023-01-27T15:24:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loop-invgen/seq-3.i
    file_hash: 6c770a3141edeab927df0da4e8c2152e1fb2e87b0c43a352500a7e3d3cff4533
    line: 42
    column: 9
    function: main
  loop_invariant:
    string: (long long )j1 >= 0LL
    type: assertion
    format: C
