- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fed90df9-ac8b-4634-80a1-c018a8ffa47c
    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/hh-ex1b.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex1b.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex1b.i: 7ce79fe11836d82ec064e02fff135ad9866417774e7d276b3384b4d4dde863b5
      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/hh-ex1b.i
    file_hash: 7ce79fe11836d82ec064e02fff135ad9866417774e7d276b3384b4d4dde863b5
    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: 494c017b-2a97-4b1c-a8ae-6a8c469d90ed
    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/hh-ex1b.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex1b.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex1b.i: 7ce79fe11836d82ec064e02fff135ad9866417774e7d276b3384b4d4dde863b5
      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/hh-ex1b.i
    file_hash: 7ce79fe11836d82ec064e02fff135ad9866417774e7d276b3384b4d4dde863b5
    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: 981c803f-f3f8-46cf-8a87-1071d06666d1
    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/hh-ex1b.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex1b.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex1b.i: 7ce79fe11836d82ec064e02fff135ad9866417774e7d276b3384b4d4dde863b5
      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/hh-ex1b.i
    file_hash: 7ce79fe11836d82ec064e02fff135ad9866417774e7d276b3384b4d4dde863b5
    line: 18
    column: 11
    function: main
  loop_invariant:
    string: i <= 99
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8ace7dc7-bd4b-469d-86c6-60dbc9a07f70
    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/hh-ex1b.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex1b.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex1b.i: 7ce79fe11836d82ec064e02fff135ad9866417774e7d276b3384b4d4dde863b5
      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/hh-ex1b.i
    file_hash: 7ce79fe11836d82ec064e02fff135ad9866417774e7d276b3384b4d4dde863b5
    line: 18
    column: 11
    function: main
  loop_invariant:
    string: j <= 100
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1274cbe8-5457-466d-8327-500df63373ad
    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/hh-ex1b.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex1b.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex1b.i: 7ce79fe11836d82ec064e02fff135ad9866417774e7d276b3384b4d4dde863b5
      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/hh-ex1b.i
    file_hash: 7ce79fe11836d82ec064e02fff135ad9866417774e7d276b3384b4d4dde863b5
    line: 18
    column: 11
    function: main
  loop_invariant:
    string: 100LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d760fa34-3850-43c9-9ce8-53f051b8bdaf
    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/hh-ex1b.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex1b.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex1b.i: 7ce79fe11836d82ec064e02fff135ad9866417774e7d276b3384b4d4dde863b5
      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/hh-ex1b.i
    file_hash: 7ce79fe11836d82ec064e02fff135ad9866417774e7d276b3384b4d4dde863b5
    line: 18
    column: 11
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a20ce010-ce87-4c24-8bda-54a48b24f63e
    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/hh-ex1b.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex1b.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex1b.i: 7ce79fe11836d82ec064e02fff135ad9866417774e7d276b3384b4d4dde863b5
      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/hh-ex1b.i
    file_hash: 7ce79fe11836d82ec064e02fff135ad9866417774e7d276b3384b4d4dde863b5
    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: c2581da7-d296-4abe-95f1-ac1626d72638
    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/hh-ex1b.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex1b.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex1b.i: 7ce79fe11836d82ec064e02fff135ad9866417774e7d276b3384b4d4dde863b5
      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/hh-ex1b.i
    file_hash: 7ce79fe11836d82ec064e02fff135ad9866417774e7d276b3384b4d4dde863b5
    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: f474f701-7d68-49ca-9c93-d67515fe5ac5
    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/hh-ex1b.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex1b.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex1b.i: 7ce79fe11836d82ec064e02fff135ad9866417774e7d276b3384b4d4dde863b5
      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/hh-ex1b.i
    file_hash: 7ce79fe11836d82ec064e02fff135ad9866417774e7d276b3384b4d4dde863b5
    line: 16
    column: 9
    function: main
  loop_invariant:
    string: i <= 100
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 501db250-dee4-4cd9-88bd-6736f71b95b3
    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/hh-ex1b.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex1b.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex1b.i: 7ce79fe11836d82ec064e02fff135ad9866417774e7d276b3384b4d4dde863b5
      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/hh-ex1b.i
    file_hash: 7ce79fe11836d82ec064e02fff135ad9866417774e7d276b3384b4d4dde863b5
    line: 16
    column: 9
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
