- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e0a0835-1ee0-4cbb-87c8-bb527df052aa
    creation_time: 2023-01-27T15:24:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 26
    column: 8
    function: main
  loop_invariant:
    string: -1 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a6e93e74-090f-4ea6-8600-eed6fc298c61
    creation_time: 2023-01-27T15:24:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 26
    column: 8
    function: main
  loop_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 37443cb7-60df-4b66-8300-b097874fd215
    creation_time: 2023-01-27T15:24:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 26
    column: 8
    function: main
  loop_invariant:
    string: i <= 4
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 212a0fe4-52fe-49f5-908a-48a71393d75c
    creation_time: 2023-01-27T15:24:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 26
    column: 8
    function: main
  loop_invariant:
    string: j <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1c658660-588f-4413-8da8-9ee75dc3d9e1
    creation_time: 2023-01-27T15:24:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 26
    column: 8
    function: main
  loop_invariant:
    string: 4LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ec93cc73-6d39-4ce3-8cf3-bfd5c61f00ff
    creation_time: 2023-01-27T15:24:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 32
    column: 8
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1c99a281-3cb0-410a-af8b-91d979fa8fdb
    creation_time: 2023-01-27T15:24:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 32
    column: 8
    function: main
  loop_invariant:
    string: j <= 4
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f4419f4e-7efc-4085-9115-c29dcae310f4
    creation_time: 2023-01-27T15:24:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 32
    column: 8
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d1554fd1-7da0-47d4-aef2-0596a0b280ac
    creation_time: 2023-01-27T15:24:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 18
    column: 8
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 18ae2cd4-7124-4e92-851a-59c2afa1e167
    creation_time: 2023-01-27T15:24:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 18
    column: 8
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
