- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 08d21b6b-ee9c-432a-bc4d-fe0a75e73e34
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f6eda85c-dba3-4555-8013-9834d4a227b9
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 47d8a94a-eb9b-4b3c-bcd7-ad8e92edbf7f
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ade91537-c007-404d-8d71-94b6709e2f94
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: c <= 32767LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fbc9cec0-b16e-41b4-93ea-f63e8d5b13a9
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f1319f8f-aeac-459e-a94f-e7622a9f5968
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (0LL - c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 15c6e2e1-59f9-4920-993f-58933aedefa1
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (1LL - 2LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 34166cc8-033c-4559-a992-d1cec0323a10
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (3LL - 3LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a5e6dfa0-f392-4c6b-8c98-4b684ce92b0b
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (6LL - 4LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b0756298-5560-432e-afae-de0337ab2a8c
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (10LL - 5LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5dd50cfa-930b-417a-bf38-fbd569aeab94
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (15LL - 6LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1f7b6a53-203c-4ac3-a2fb-aaa0c4ce8a5e
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (21LL - 7LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4456d05b-a186-4136-ba6d-914e13fbc5f3
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (28LL - 8LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 487a2d7b-0108-45ea-91da-e9e224bf7b40
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (36LL - 9LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: def91dd4-a6e7-42eb-9a64-272a09ea9be0
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (45LL - 10LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0fd58780-27d1-4e55-8740-574f3b3a16e0
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (55LL - 11LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1cbe40fa-83b9-4884-9ae3-f2f0629a19d2
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (66LL - 12LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b35ac51c-d563-427f-b35f-945336989f66
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (78LL - 13LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ba740906-5a0c-4ca8-9b33-58fb2dc48923
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (91LL - 14LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 81dae2ee-6dc0-4ae8-b199-535227d31d30
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (105LL - 15LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 39b6485f-4f7e-480d-9255-c6fa9bd25095
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (120LL - 16LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e7b5b4f1-6893-42e5-be5f-cc17aa0501d0
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (136LL - 17LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 315b647a-de7c-4acc-ab7f-6441a8c171c1
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (153LL - 18LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7828a6f6-fb4b-4147-bc42-f5c8728f2f2a
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (171LL - 19LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e6e07f23-7611-46e8-9d34-f6a65817616e
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (190LL - 20LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d1d2146-81ca-47d4-84d2-e70da33dd807
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (210LL - 21LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c0500d8-dd19-47b5-8f8f-d5659000147c
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (231LL - 22LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c53cce5-396e-477a-ad4c-86c9c266237c
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (253LL - 23LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a52ae24e-30c8-43e0-ae3d-1113b6fcd20e
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (276LL - 24LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b364178-82b2-4d9b-bc2f-a43a70b94896
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (300LL - 25LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c2047ee1-4e40-4513-b710-65435cc9b688
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (325LL - 26LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9624f3b8-6c9f-4f4a-9ad6-90b76eba5938
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (351LL - 27LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c0bd2f34-6e93-4fd2-953d-e6c139db7560
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (378LL - 28LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 35d730c3-3149-43be-92b9-d2c4f4473a84
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (406LL - 29LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8ba4818b-262e-43a7-a072-bda9b0a035e0
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (435LL - 30LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cdef933b-ac52-485e-8bb7-a84788bb9ede
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (465LL - 31LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 96b3b307-8648-48b7-aa21-2818b3a22264
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (496LL - 32LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d88d8f69-020d-4b6a-bffc-74af6691c8ea
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (528LL - 33LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a98b95b6-f79d-45a0-bdba-19af004df4b5
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (561LL - 34LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 228bff94-07f9-40ba-816f-5ad76fcf8f03
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (595LL - 35LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 44badff9-2634-4110-af56-d2e3e276eb46
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (630LL - 36LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f7e415c0-3ed4-4243-9fbc-b7b91372f510
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (666LL - 37LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 25035745-2053-4b4e-a25c-d96390e275eb
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (703LL - 38LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f921740b-fc22-4d41-9040-f32c365013c7
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (741LL - 39LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ebc1b773-bdde-446d-a8b1-7066af61dd84
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (780LL - 40LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e5a38b4-b12d-484b-b17a-b66b20fb0450
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (820LL - 41LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6af3ef73-6632-4454-bcde-dc5fde8d75c1
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (861LL - 42LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 76fae6fa-6a5e-4962-bc60-fc5e6f5adb77
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (903LL - 43LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c39eda99-0564-48ba-aa1c-c8f0c26a2c7b
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (946LL - 44LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e7701b5-1912-45c9-bab6-3cf140400cec
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (990LL - 45LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4b52ae87-c9b0-412d-b62d-39312140fab2
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (1035LL - 46LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e3fcb5f-816c-4dbb-9807-003f5d2d5467
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (1081LL - 47LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f3347d33-32c4-47bf-9322-eafbf14e53ef
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (1128LL - 48LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b0c431c6-1a3a-4c59-9cc7-37d5f0dedb5a
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (1176LL - 49LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c9992ad8-9afd-4ce2-8945-57e95218fc89
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (1225LL - 50LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1f3d2197-34e0-462e-adcb-822f669ebfc5
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (1275LL - 51LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 74463feb-03dc-4bda-b343-67a04d343971
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (1326LL - 52LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 72a6ad87-a5fd-47a9-9a5f-491ae68db51e
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (1378LL - 53LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ca6115d9-9fdb-42af-b492-c00c9244bf69
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (1431LL - 54LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 278eb335-ca95-4d75-9737-02488aa2136c
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (1485LL - 55LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 12d2c780-b33c-43ac-a751-3ad88697043f
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (1540LL - 56LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4edcc7a6-06d2-47cd-9d61-1967ecc21519
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (1596LL - 57LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c604f7c5-c7ab-48a2-b30b-dc09a194efb4
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (1653LL - 58LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 30a6249a-d871-453d-bbc8-e78f51986cd5
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (1711LL - 59LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 67e3399a-7c4f-4430-9f67-1389839fccec
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (1770LL - 60LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d0330f5-28b1-401b-8610-ed668a1a2a14
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (1830LL - 61LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 27a96996-06a8-40b8-a07e-bfdeb7d87c4c
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (1891LL - 62LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d855e34-e0a3-4c69-8b4a-3981af4d945d
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (1953LL - 63LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 91bf095a-aaf4-4269-9227-f5b8f169aabf
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (2016LL - 64LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c5167808-4600-454f-8a6b-324e5a2c32bb
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (2080LL - 65LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: aa631a92-adcf-4a18-bbb4-5175f1b59aef
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (2145LL - 66LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d2bed236-b76c-4ab4-877a-ebef96847ac9
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (2211LL - 67LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 80f083d4-af3b-4259-ad68-c1316b82edd0
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (2278LL - 68LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4f51ba56-4d0a-44ef-80eb-7f69ebcd6164
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (2346LL - 69LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bd038f21-987b-477a-8e72-dcee788d1ac7
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (2415LL - 70LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ba3d64d-93c7-4b47-94ad-13cfeed12347
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (2485LL - 71LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c0becd8f-8ccb-41aa-b1bd-bc7a3e6c9605
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (2556LL - 72LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c4985170-c57a-4dde-bb35-2c8332c46ae3
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (2628LL - 73LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: da4e98b2-d027-4540-bdfa-74dc170fb8c8
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (2701LL - 74LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 85903ea2-fbae-4db6-8674-ffaddde920ab
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (2775LL - 75LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f7b28cf-498f-4d6b-b103-aecfcc082234
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (2850LL - 76LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bc2aeba2-50a6-4352-b747-19b09ec960de
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (2926LL - 77LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ff050afb-753a-4f46-b907-b78a5441e807
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (3003LL - 78LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1af6f591-488d-44bf-9b2d-3c1ca1ae6903
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (3081LL - 79LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bc340226-9ca2-47a1-95bc-a7a6e5424f7c
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (3160LL - 80LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 69cc7bb7-28ba-401f-9c6e-8bb3ed8cbca4
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (3240LL - 81LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f4e417f-0ef0-471c-a1f7-a22cf27f0514
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (3321LL - 82LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fcf2f853-b7b6-4d54-850e-63cd85854ea4
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (3403LL - 83LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d770b65-cb84-44be-8aab-66dc397b0738
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (3486LL - 84LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b3563ed2-c61d-4fef-a242-0284454bd669
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (3570LL - 85LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fa933760-30b1-47db-9e10-a24c9a91d390
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (3655LL - 86LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 80f7e732-160b-4b2a-822c-68eb3a94eb21
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (3741LL - 87LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5dcfa5da-9ee7-46c8-af55-09d2956ca6d0
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (3828LL - 88LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 011a4af8-6833-49ad-a7be-6dd662a4ca8d
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (3916LL - 89LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 649a31c0-bf98-4c17-8ff9-c0ce4c15453d
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (4005LL - 90LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b06c8be0-f2e0-467d-8483-c5972845c8c1
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (4095LL - 91LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d3617b9-bcf1-4b71-949e-3c7ffe2eec3e
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (4186LL - 92LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 01dfeee4-05d8-4b3e-8c0d-ae551ee8084f
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (4278LL - 93LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d314b1a2-865c-4230-9cad-4a98db8e133a
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (4371LL - 94LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cf474580-e5ce-4bb3-8314-9a7bf8e8dd9a
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (4465LL - 95LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ee46929-614f-48be-ae02-9b9a3e0ca7b6
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (4560LL - 96LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 34d1ab2b-9d3c-42b4-8503-83da1d575fb9
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (4656LL - 97LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 51b9f264-4c22-47e4-bee8-596bd9d07920
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (4753LL - 98LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 330ef2d2-7dd6-40c3-ba5b-e103a31af9ee
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (4851LL - 99LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 22691eb7-7de4-4660-8945-ca0d10ef7169
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (4950LL - 100LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8bd4d995-07de-4990-bbde-8f8f61afd135
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (5050LL - 101LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8207b971-d74a-4ca8-ade4-14462be07500
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (5151LL - 102LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: caecc7d8-8d9d-4da6-b63b-792d02b2bc5c
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (5253LL - 103LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c98e132-bfca-459c-b359-d04107426c28
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (5356LL - 104LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e3598e6-944e-4310-ad2b-214f377017dd
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (5460LL - 105LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d23667b7-4eed-4569-8a92-7ede3db3e3aa
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (5565LL - 106LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d54d24c8-3529-403e-a80a-79251d9c3518
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (5671LL - 107LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0d0709bc-a4f5-4327-a1db-cd76026c8be4
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (5778LL - 108LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c2b90941-39ea-45d3-8b76-f716154a8e22
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (5886LL - 109LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f76a9556-16b8-4f10-801b-acb9fcea33f6
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (5995LL - 110LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9391c302-b37c-454a-bdda-18243b10c5a0
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (6105LL - 111LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9fb19c5b-3e45-4e44-b12d-7d05f42da673
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (6216LL - 112LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 65b2d554-256f-4186-9d1a-3e8e35599c1d
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (6328LL - 113LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a0528eb-94a6-4179-9ae0-6e4bdd7f345f
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (6441LL - 114LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f67cb4f2-78d4-43c6-9992-ba1c7e397e3d
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (6555LL - 115LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: df5731f6-ffe3-485c-ac41-d96d521ccbd9
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (6670LL - 116LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 032dcb40-e0b0-496e-8f45-fb1e18cc0ae6
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (6786LL - 117LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9cee4e6f-e7c5-4285-a648-be6d4a19250c
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (6903LL - 118LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b57a1912-57cb-4f8b-8300-3d021daa291a
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (7021LL - 119LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 79d7bc5d-3e12-4fc1-9d0b-9e79f5b8daff
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (7140LL - 120LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 31caa43f-936c-4002-8494-80748fa53c74
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (7260LL - 121LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 18cfb2df-0aae-474a-85da-fc907ce94cf3
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (7381LL - 122LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 618b4a47-6b10-4a9c-bb0d-2e8a3929c08b
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (7503LL - 123LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a9802e0-13be-4af7-a001-04097e17ff67
    creation_time: 2023-01-27T15:25:01Z
    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/nla-digbench/ps4-ll.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/ps4-ll.c
    file_hash: ef01badb7f90b6597aa83d48583be40b7afc9a4c054f915d626bd89be70c7009
    line: 26
    column: 11
    function: main
  loop_invariant:
    string: (7626LL - 124LL * c) + x >= 0LL
    type: assertion
    format: C
