- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b08c0ea-1b3b-423a-a1a3-d5c300e86c27
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7df96208-4d02-4dfb-b652-65f3a2a4db8d
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 08fcee1c-9767-4d30-bcc8-eab226317451
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0dc292f5-f1e8-44ae-a969-a038294f77c9
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    column: 11
    function: main
  loop_invariant:
    string: c <= 32767LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9fedeaaa-cd6e-41dd-b7a2-67a83b5f2fb4
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    column: 11
    function: main
  loop_invariant:
    string: c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 298c2069-5940-4da5-90f0-57e08ada75a2
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: dd06e8cc-039c-4bd1-8e96-3881efd3a151
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 4f4b1161-51eb-4688-b69a-4343538090df
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 655d6586-f4da-4ebe-991d-77235d18bb86
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 218cdde5-1fdd-4144-852a-69696c82b109
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 3f41aca9-c861-4fb0-adb7-bf589eab613b
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 64bc7b1c-a85b-4c93-bffc-156bf13f55b2
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: eb9b1ce3-53ea-46ac-8256-01ba39dd607d
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: b74d5269-e278-418f-8319-d637c174a6a4
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 92a1e85c-4f4e-4e40-985e-7be846c69426
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 51747bc3-594c-43ab-b9c2-44fb65c8a620
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: dd95f7a6-9aec-4056-bfb9-b9a0429ad040
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 3a420d2d-c017-4ef2-8a3e-9417ece90b43
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: b2fd034d-ed07-4876-9dee-2d01aa815219
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: d9da1948-422d-401b-8a00-f0c776eee247
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: cf305177-c1c5-41a2-8379-b7bfcafd8d50
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: d267110f-3ddd-4369-9111-0cf560f068a1
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 1bddb9df-3d53-4f32-a097-02bcaaf9fff4
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: c3dc812a-96f7-49da-b016-19ad78718169
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: c290f523-e07c-4adb-bb06-dea5afa2a94e
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: d7ba1b1c-2a68-4c94-88a0-a81247b65c9d
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 2dbc80a1-8a9d-412e-ab84-0a9cdf7f6eeb
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 51e69488-02fe-4758-a3f6-961054a6c5a1
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 93e3fa55-9dd1-42d6-b97c-e74583ecc0ed
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: adf29014-ca89-49a2-a784-25f0c09a0592
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 5f44b812-d322-4041-b5e0-6cb57dcc90f7
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 817f4646-7ce1-45bf-90a3-1f516ba6b097
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 2d05654b-f95d-4a02-a29c-a928e5fa0281
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 6fc8f519-24e8-49aa-8899-0009a190fd48
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: a07ed7c1-79f2-4917-92b4-ea81f558d3ec
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 8d7e92e3-d20d-48da-a5d0-674534c89c0f
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: da4cc079-6e20-49a2-9873-cb572723f81a
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: beb3282a-0ae4-4b81-a000-ec5e839fb656
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 0c7ee8c8-0763-4d94-8def-f402f04ff286
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 8e6468b3-65c7-4ee3-83a0-cffb1cede58e
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: a03bc4a0-4861-4a72-b1fe-171675859687
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 1c3143a7-51b5-493e-bdb3-7a884e34e42b
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 388fd636-c9a1-4b30-8912-40f9de71ffbe
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 2720851c-ad86-403d-aea6-8dade5e66e04
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 201fd829-a2d0-4576-b5a1-63aa90850139
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 9a052853-de5a-4ed1-8119-b2659628d209
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 660dc087-0ed2-4a68-9f19-c9d132e09f84
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 5ed4bd81-9f63-4e55-82c5-8086da9d6a69
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 91df9867-99ba-41c7-bcc9-8d8595df9d35
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 083d5f05-28e8-47ae-9e9c-7b4096dd936c
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 0a6975c4-849f-4f0b-9943-a059be50a31f
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: b2744757-4e89-44bd-9fdc-72e08e37e71d
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: d83abb19-5f75-4ba7-a8c1-4cee67fdbf5e
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: c913ec99-9d5f-4ab5-b7b1-a33fa4f26d99
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: a489d9a5-8c1f-4b91-a03f-487faf74f599
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: d5542c2b-df2f-4271-9dc9-4b5a2d0145cf
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 1a725f4e-47d0-4e95-a19e-516bd9c828c8
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 112d7344-8319-46be-9467-52800f537013
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 40f2e36e-da1e-4e6d-bd24-f63f9cea50d1
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 4b3ee948-ada6-4572-a667-ed4a4783d7d9
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 83d673ba-b1c1-4346-a929-9be9d525181c
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 0f0362a0-d9cb-4b32-ab22-d0bb879cfb4c
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: ec43a867-c0e8-4200-ae24-438f2d8968f7
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: f7028415-8ce8-41f7-be44-66b1cf4f226e
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 382739cc-8f43-4d1c-958c-c298c8e8ba35
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: f15a2beb-ca08-40c9-95ec-eede166245e1
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: a22e73a5-b5a3-4b39-917b-0d95569c41a5
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 358e0b58-4a32-4c25-bd78-1dabfb98f34f
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 157a273b-c7c1-4b1b-9728-3b8233960841
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: a9e9d258-dda2-4f88-8fb0-de24e15007a1
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 73ac8c8a-d4df-4b2d-94f7-3062d34565a2
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 510c7394-0ced-4c3d-a9f4-a3a9c214e332
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 56e4d14f-083f-4ccc-a7d7-73f202aa81a3
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 3fe92e9b-4ef4-4c6f-ba6e-75aaa5a60ff3
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: f252e932-0610-4823-ba0c-28d4f78abfa1
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 3b680f83-7916-496e-8569-651379c7d616
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 04fccc5e-7795-444d-a1c1-ce060e93c1b4
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 1fd1a209-c216-47c5-9d87-fadc4a40f067
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 13c119b4-2e04-4f8a-8980-5c6fd30cd252
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 971d7865-b0f0-4dab-a476-2f0aa20bc5e6
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: b3dc5a41-308c-47c1-a7b6-ee58ed78dd98
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 284ec6ca-3cef-49aa-9d70-47e33cab7b1b
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 2223c396-08ba-4387-9e6b-390a84e3ec40
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 10998768-d9e1-47e8-9e99-8abd8aa45fee
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 1651cab0-0f0e-4126-b99d-792d26038ac6
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: bba5f8d5-2388-42a3-a8bc-18726ebab043
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: e94e8c3a-5671-4ead-ac99-f1c92fb62404
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: fc94f96c-c55b-4c27-abfe-bdc17edab3f1
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 95ec9934-e5d9-4761-a190-b44ab679f4eb
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 0502bbbb-c78b-45f6-a159-3e5b6d9789dd
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: f10b0989-01bb-4469-8586-3d433f85050d
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 3ba3ef0d-d684-4ba7-8ada-76f9a9915107
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: eb910bb7-8b7b-42de-abc6-b8a7d69c3c4b
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 5e278c93-9db3-4ff4-ba30-953582a1bbbf
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: ce8ae8f8-c57b-451b-867f-64051b59a8a4
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: f93c49a5-11c9-41f5-8f64-05198041f533
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 2b83acb5-2f91-4f40-bcbe-d3e0f4f7e382
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: fa5b0c78-f960-45c8-886f-766d0a2d26ae
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 329ce04d-5767-45e9-ae89-39bc45935fc8
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: d7374785-0c66-4b04-a12e-6838e70e206e
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: c0c1367f-5274-43de-961f-ba6becfba3f8
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 9fb0137c-3e04-4a10-a798-0645a48a278d
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 1dd71b2b-5931-4f57-ba0a-083b686539fc
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: d214d6b0-e787-4143-a1c0-197f46139155
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 85d5e6be-3994-4c36-9f88-fc180cdb6905
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 3753e6b9-fdc2-439d-b18b-ca1349c1df8b
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 0bab6975-d3ff-4e71-92b7-79e59ffb5420
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: dd7bb941-e0a4-4bda-b6fc-d7f88cfe2c27
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 24e9cd7f-d07c-44f7-87c8-a7d014356516
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 6d98bf31-6c3d-47ae-bf71-c1ec05adc30e
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 618d2115-e24c-47d2-ad67-fc696f0b527a
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 3fc745b5-a55a-498e-9a1d-7d0278c6b441
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 683c2d6c-e96d-4378-b66b-06cf5b04132d
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 66f74311-d5ea-478b-95ea-ac14653d2189
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 063c2bdc-d055-44d2-b590-96620fbb6d6a
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: edeba625-d253-4b6a-97f4-39b77d9c510b
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: e861f719-8be4-4b9a-b96d-17dab0bd2dfb
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 592565b1-9a45-442d-bb5d-d47abd786098
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 7dbd87b4-1cd2-4d2d-8ae6-455bf8040283
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 48168bdb-c7c0-4805-af9e-924cffe17c7b
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 9b219d30-a868-488d-b442-17bc9643351e
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: e2f73003-cef3-4de9-a939-50dc634510f8
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 8ed20189-0752-409c-86a8-619fe5dd83f2
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: a63752be-0ed3-4414-8a06-4cf8b8d87aea
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: dc8f327f-9272-4c35-9307-7f354b838881
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 10bf840e-e7e0-4ea3-be58-577fad4dbf69
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 7267a4d3-f3f0-4391-9f9c-a233c0b3ffa1
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    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: 2080c3ee-8215-4189-b73b-0bb1ea0d175f
    creation_time: 2023-01-27T15:26:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/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/ps5-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps5-ll_valuebound5.c: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
      data_model: 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/ps5-ll_valuebound5.c
    file_hash: e14135f4afb726bf8552a88de51bf2d1eeb5945775070b599f71e8288a74bc87
    line: 28
    column: 11
    function: main
  loop_invariant:
    string: (7503LL - 123LL * c) + x >= 0LL
    type: assertion
    format: C
