- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2516f57b-6345-4511-bfb9-899abd6111b0
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 76887009-2500-491e-be79-3aab2821d66c
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 759ed006-4cdf-4fa8-bc2d-4663f3ccbd95
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f0274cdb-0e69-4ec8-8ee5-c41d2a59f7a9
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: c <= 32767LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c555af1b-52ef-4ec6-830b-105abf992f81
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 68d4f40f-e36c-426e-9d9f-030c503da2d0
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: e4c693aa-777b-4292-ad03-82bffc760a63
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 833bb774-dc9d-4677-9705-01b284d845da
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: c588a844-26bd-45dd-8969-4990e3344d0a
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 64725b5b-971b-4190-9633-6196158f5b04
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: e099ae57-7b25-4bce-a306-8f64bb9dc38a
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 5f9769c9-373a-4b1d-919c-f6075d650f00
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 1759b6f9-eb93-44ab-80f0-b53f2ca39369
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 8701dc94-8796-4d2a-920a-e4e5f8cd671a
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 2a02a999-9711-4613-b40c-82fc93a2708d
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 1d602d68-c44a-4322-84a3-2bdaf2fac196
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: cdd899e6-7c1b-46b7-b81a-29e356cc0d8c
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: ac51980a-0fe5-464d-983b-bcd4986d1cc0
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: ac3bab96-3554-4475-abf1-944b758e9906
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 69f277dd-2799-456d-b6f1-dfc2ed182f03
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: e58c0385-99c4-4934-9ccb-72a921114998
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 51274877-db52-4647-96cb-d9885ec99a7d
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 062e6da9-10d4-4efb-a818-12cc778ee756
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 26e5999f-3d2c-46b5-b7ff-9a70675f6d02
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 9cc14c2e-c341-43b9-873f-3872ea62c88f
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: d708a903-8a89-42e6-aa33-1b688582317b
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 2f637956-514e-4da5-ad3c-f0f5bd6d6db8
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 2571e13e-a463-4922-8ef6-7b2f22a688ea
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 56cf9717-3d52-46ea-a74b-90c0b17fd937
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 8d926bb2-1aee-4dff-a12e-c10e7529f56d
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: e4f4b463-e9e5-47a4-bab4-21892d51a1ed
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: b81c3a68-a26d-4a3d-9e55-fc98552cbf1d
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 81a2faab-3ecc-42a2-b41c-28319bb9793b
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 86e681d3-81b5-4e2d-81bd-75e46d0a1f79
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: c2cf46da-0cc4-44c5-ad3c-ed63b3ef36b4
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 5ef94bbc-55ad-476c-b55a-267b1924d304
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: bc7608e6-7e3e-4656-921d-010e3aa4a9a8
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: d2502810-6e88-421b-b8df-5d39136a050e
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: e98eabb3-465e-40d0-a134-48db3ececb85
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: d20a0592-23d4-46cc-96cd-45f26ef5aaa5
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: ae0bd266-ea34-4dc9-b63b-85c5b1165321
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 33a971ce-e231-4975-810a-cf0888772907
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 8d219a29-1976-4518-95d4-3ade722dcd57
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 3b4bfe74-8ff4-4dc8-968a-b0457a17aa4e
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 8bf4c2ad-1061-40e0-8103-d4c1a252ecb7
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 9855ada2-17c9-4365-a460-c14b81352823
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: f09e556d-617f-48dc-8244-5b2d55a994b6
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: fc975730-28b0-4b2d-ab00-33864473b630
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 0858fb8e-8f22-4030-adf8-d338e7a4f380
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: c6e619ee-915c-4634-8fc4-3c93c97e0a00
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 6f59dc14-1897-4874-a6de-a6d772c98048
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: aac306f8-3fe2-4974-ba53-4e2512d89ca2
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 51cc23b2-8187-44e2-aa6b-4ef4ccd2545c
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 27d8102f-b1cd-4442-80fc-eaf47260539c
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: d77b796a-e7ef-4651-b61a-d38d72ebe335
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 8e75316b-f77a-43ce-b895-30fb668f8681
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 90552b12-71a5-458b-bd78-58b75fdc0596
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 7de7b123-2586-47d5-8c84-3daba8f7bac8
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 873adc76-f4d3-4eea-9f81-ba68b0c195fd
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 68b477c5-6733-4155-92a9-a17de38feef3
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 2a83fbcc-0dd6-4b9d-b6ab-2ce0e3519972
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 5a8f58a6-8dc8-4dd2-9ad5-219f08fa96af
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 2b45ba8c-950d-447b-afc4-f3bd8a304d02
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 55629f25-6939-461a-b191-d4ba51100805
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: e1a05fc4-eba9-48b8-aff0-bee4f41aba4c
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 5a79c7e1-9b67-430f-9882-06d81b8d6319
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 8269009c-7a76-499e-94a3-069312bc7d65
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 2ec89462-00fe-413b-8b06-217e35fea79e
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 0b979d4b-6a40-4d5f-a01a-4b376deb6053
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: d33c3db6-5673-4d0a-a5eb-f3974196564f
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 76b9ebb6-0893-4520-bb95-4b31d44edae8
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: f2cf9e1b-879d-4367-a947-94066658648e
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: a7a86422-f7c8-437b-b350-983bac0031c2
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 9eaabfb4-5da2-49ce-a1c4-f1e69051c637
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 01011531-00d7-494d-8ffb-140c6c5b4072
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 5bf4dea3-28e7-4765-bd47-3204e00e448e
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 97c8256e-5553-43b9-ad8a-99e0b0d89bed
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 6b52ea82-4a15-4eaf-a72a-a4025a5074cb
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 98568b21-a962-4160-befd-e9f18596f24a
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 4b5945e3-1400-4903-a978-ed0632dd56e4
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 9a749cb1-5788-4d49-8feb-cae63cab62bb
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: b12b4b17-fd71-4ae0-b3bd-32921b81d0c8
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 3c5ed8a9-4fc3-4ce1-ac9c-e7bef0f1493f
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 3b96bfa6-49b3-47e4-a19a-ade5d6a4221c
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: f7751d48-b42d-4bff-a36d-545a8e3bb9bd
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: f34b8b70-591c-412d-a810-150ee44857a4
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: a7d8af52-9d83-432c-8a9f-ba5ecbd928cb
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: ed83df20-819e-46c6-9887-0bd56e0b3009
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 321be3d1-a8ed-4e65-b47a-6700f73720bc
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: d9955a5c-3f22-4c25-8647-9dd72044d421
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 6a753de6-8a1d-425f-852c-1b05a031b472
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 483292aa-a313-49be-8044-e71d4dc0789f
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: ffcf87a9-d521-484b-965b-b6b4ba3b3694
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 5429bd9c-d3a2-4617-a31e-866a78fd1fae
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 669f9bd7-6496-4cc5-b043-9b4a510c2d13
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 03326d1e-4a88-444a-bfad-7666d5d880de
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: c26da6d2-ce59-471f-aa9b-327110644a44
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 654bbc8b-cf15-40d3-9342-ce0510c15118
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 6123e23a-5126-4f73-b05d-2d25cac1e4c3
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 56afb52a-d2aa-481b-8b4e-0a2b15be9b34
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: f44335b8-debd-47fd-b3ab-338964df1473
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: a6886dea-bc8a-4d7b-b976-a3614da82248
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: ce10cc70-11ba-4190-9813-4136e8f2eeaf
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 3d14f60a-21de-45cb-862a-cc87fd093ca4
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: a94162f8-f684-4a40-b26f-acdfd52a3178
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 4f63b317-144c-4507-9916-466c9f165928
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: a166baf8-8dbd-440d-b78c-3475810c0c43
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: f2e0cd7f-57c7-44f4-b757-bde98607b091
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 9d93a161-e0e1-434a-9554-88ac23028d00
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 56d3487a-651c-4275-867e-0b0af58d6bc1
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 7e5349e7-130d-4016-b545-8f6e846a6b0a
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 25bcd1f2-4171-44fb-88bf-7f897a257912
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 09b15b8d-2345-485f-ae04-6180d9dc99c9
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: d353e562-f287-4d1b-9d6b-081d40b0d336
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: dca50c9d-b47f-4129-8a0b-aed75192d3c7
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 4742fa43-cacd-46d3-a4d4-c8365436496d
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: ac24d59b-6795-45f2-a929-5382e4a5beac
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 27713207-4a8f-4108-8bce-a568418c8cbd
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 60f30b86-0823-457c-807b-02548b68276b
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 315d9333-34c7-45a2-8346-10c58e0aa840
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 2b0ab73f-0b29-4413-a733-8b3d003c3813
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 411bdf36-5607-444f-bc0f-5d445933b35e
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 7429fca4-6646-469a-be27-1583a478e5f6
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: c75db4b0-9477-4f4f-bf4e-f095a782ee0a
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 571124d4-e593-4d9b-a273-2b82bbb227c2
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: fc1000be-1113-4c5f-803f-756598a29756
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: 0683426b-d484-4300-a8e0-f14a87c1826d
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    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: ec3789c2-8274-491c-ad80-5ae8f302fa05
    creation_time: 2023-01-27T15:25:48Z
    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-scaling/ps4-ll_valuebound2.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps4-ll_valuebound2.c: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
      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-scaling/ps4-ll_valuebound2.c
    file_hash: 68d290aa6e6a124b20d02df1a641bd7e739f143db7416cdcc7b7048aed53c326
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (7503LL - 123LL * c) + x >= 0LL
    type: assertion
    format: C
