- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f30227af-d243-4b29-bab3-e3881d56b79b
    creation_time: 2023-02-16T10:30:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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/bench/thread-witnesses/st-lit/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''64bit'' ''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i: d6dbcbf51695ea037a123bcc006ce5f6db095b874a22b169ec869d834ce41de6
      data_model: LP64
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i
    file_hash: d6dbcbf51695ea037a123bcc006ce5f6db095b874a22b169ec869d834ce41de6
    line: 18
    column: 11
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f8dadf4-b6e3-4d0a-a521-a49c7fb197a1
    creation_time: 2023-02-16T10:30:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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/bench/thread-witnesses/st-lit/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''64bit'' ''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i: d6dbcbf51695ea037a123bcc006ce5f6db095b874a22b169ec869d834ce41de6
      data_model: LP64
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i
    file_hash: d6dbcbf51695ea037a123bcc006ce5f6db095b874a22b169ec869d834ce41de6
    line: 18
    column: 11
    function: main
  loop_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8704b851-80f5-471f-80b2-ca5f727998f4
    creation_time: 2023-02-16T10:30:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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/bench/thread-witnesses/st-lit/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''64bit'' ''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i: d6dbcbf51695ea037a123bcc006ce5f6db095b874a22b169ec869d834ce41de6
      data_model: LP64
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i
    file_hash: d6dbcbf51695ea037a123bcc006ce5f6db095b874a22b169ec869d834ce41de6
    line: 18
    column: 11
    function: main
  loop_invariant:
    string: j <= 4
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 64d2163c-47b1-4ef6-9c69-b7cd26395485
    creation_time: 2023-02-16T10:30:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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/bench/thread-witnesses/st-lit/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''64bit'' ''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i: d6dbcbf51695ea037a123bcc006ce5f6db095b874a22b169ec869d834ce41de6
      data_model: LP64
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i
    file_hash: d6dbcbf51695ea037a123bcc006ce5f6db095b874a22b169ec869d834ce41de6
    line: 18
    column: 11
    function: main
  loop_invariant:
    string: 4LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d856af82-1810-489f-8850-a67f4b341e32
    creation_time: 2023-02-16T10:30:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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/bench/thread-witnesses/st-lit/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''64bit'' ''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i: d6dbcbf51695ea037a123bcc006ce5f6db095b874a22b169ec869d834ce41de6
      data_model: LP64
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i
    file_hash: d6dbcbf51695ea037a123bcc006ce5f6db095b874a22b169ec869d834ce41de6
    line: 18
    column: 11
    function: main
  loop_invariant:
    string: 2LL * (long long )i - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: aaf78f48-6ecf-497d-b897-1ea3f1832ef5
    creation_time: 2023-02-16T10:30:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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/bench/thread-witnesses/st-lit/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''64bit'' ''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i: d6dbcbf51695ea037a123bcc006ce5f6db095b874a22b169ec869d834ce41de6
      data_model: LP64
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i
    file_hash: d6dbcbf51695ea037a123bcc006ce5f6db095b874a22b169ec869d834ce41de6
    line: 18
    column: 11
    function: main
  loop_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f723434b-8a92-46a5-8d74-6e660e61dad9
    creation_time: 2023-02-16T10:30:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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/bench/thread-witnesses/st-lit/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''64bit'' ''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i: d6dbcbf51695ea037a123bcc006ce5f6db095b874a22b169ec869d834ce41de6
      data_model: LP64
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i
    file_hash: d6dbcbf51695ea037a123bcc006ce5f6db095b874a22b169ec869d834ce41de6
    line: 16
    column: 9
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 42e089fd-8a5d-4552-927f-bec6cbfd2b6f
    creation_time: 2023-02-16T10:30:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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/bench/thread-witnesses/st-lit/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''64bit'' ''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i: d6dbcbf51695ea037a123bcc006ce5f6db095b874a22b169ec869d834ce41de6
      data_model: LP64
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/bh-ex1-poly.i
    file_hash: d6dbcbf51695ea037a123bcc006ce5f6db095b874a22b169ec869d834ce41de6
    line: 16
    column: 9
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
