- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c71971cf-0f1d-41e8-9da4-45957413c7d6
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d7f3a250-1d57-4655-9f5b-7fbbbbc7b0f4
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ffd95e7f-bb46-490b-9e42-f84bee9565dc
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a9b93af5-191c-4563-9e48-cff678b0adab
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: c <= 32767LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ef5fdc5f-7e56-4926-8c1d-a4867a08ca4e
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 19e82c02-8951-4fbd-b59f-b6a8dcc7041f
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (0LL - c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 492f760c-4fbd-4983-bdab-69b5a3a94323
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (1LL - 2LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e92fce85-d745-448a-938a-ab81af0fb87a
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (3LL - 3LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d5c3e665-ac43-4ac6-beec-8330cb8f1421
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (6LL - 4LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a438904c-29bc-4166-b21b-d74a3f107a94
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (10LL - 5LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a23e6bbd-265f-4202-804f-322c75368c12
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (15LL - 6LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8a680af8-f749-47e8-9c2d-975914ca72b3
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (21LL - 7LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d9124b8c-4ccd-4666-a9aa-3c3567315d98
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (28LL - 8LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2cfddd54-eb14-4b89-b319-3ee87841f18b
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (36LL - 9LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f3498d4-dd02-44d1-b9f4-12c56534d576
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (45LL - 10LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1281c9ef-b6e6-456c-be46-600296df0c8e
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (55LL - 11LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 847cbebf-c7bc-4664-a8c6-15ab2bfa2e94
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (66LL - 12LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cd41eb92-b7c7-4995-84a3-b39bd140b837
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (78LL - 13LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5be3e768-ea90-470f-8ad7-78e8594cede1
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (91LL - 14LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f5c2e94-a921-402d-a9d8-98c8e4cdfb99
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (105LL - 15LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9bc489c3-5d54-4f53-96f9-d919342341fa
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (120LL - 16LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 76b541b6-a728-45f1-8605-19a0bb96a1a8
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (136LL - 17LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a6f6b37f-7408-4aa5-a3f5-53c1dadf28df
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (153LL - 18LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fea62964-8eb8-4e04-9362-04d20ae5dd69
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (171LL - 19LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f634279c-cefc-4af8-9a03-cf0650bad0e5
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (190LL - 20LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e1627f5-3931-4161-b99e-34f93dcd8a5b
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (210LL - 21LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 061bf888-7b70-4536-ada4-b4648fb91fc2
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (231LL - 22LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: de768432-7dfe-4d26-8d6e-3e9b3113d14f
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (253LL - 23LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 77ea3f2c-ae7b-4f16-be18-bc34c7947a12
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (276LL - 24LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7cc2fb79-91ba-496e-b965-31f4bb50b7ec
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (300LL - 25LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 06c6b68a-de48-48d5-b4a6-95b9e89c03ea
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (325LL - 26LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6caacf32-747b-4e4d-8833-0b67d2574738
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (351LL - 27LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f710e6aa-c220-457a-9b81-89ed5f4b0a38
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (378LL - 28LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: dbb88040-eb8c-4be6-a172-52ff481ed410
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (406LL - 29LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c8f69eea-78f8-4539-b210-80ee22a10231
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (435LL - 30LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c475015-91f8-4c6e-9495-8970b5ebb5a1
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (465LL - 31LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 10039bf3-ffe7-4507-a17d-7db9e4624444
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (496LL - 32LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1c05e1ee-2540-4852-ac18-30c8c2c47d94
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (528LL - 33LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1daf1723-8ee4-47ca-b230-5f18b39cb3af
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (561LL - 34LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e224efe-66fc-4849-8a03-49183ae7625b
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (595LL - 35LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 50d3222d-8859-4a5c-afde-292eccd0920f
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (630LL - 36LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ef7d3fa-2599-43e4-8137-8e1d7e26799f
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (666LL - 37LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a4c663d-7716-443c-ad33-f3834fd5031d
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (703LL - 38LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f5527d4-c701-4b65-a3a7-c935787bd5fa
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (741LL - 39LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c4da562-9aa4-4719-9901-37aa797ddac3
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (780LL - 40LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ba65f6e-9b46-4b1e-9b77-7c3026ea306b
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (820LL - 41LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b3a29763-641b-4b91-8e1d-e3cc9315d46d
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (861LL - 42LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9c12b0ff-f6bb-4e11-a5a3-16851cf179c2
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (903LL - 43LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8fa4b514-72a6-4181-a08f-4607f6b7fbe3
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (946LL - 44LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0ecc0d67-e30b-42a7-adf8-606f5a66eb27
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (990LL - 45LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 491d2146-b4a1-4dae-819d-ed273b1e24d5
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (1035LL - 46LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2197e6ab-2eb9-46b9-ba79-7052434dbf35
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (1081LL - 47LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a62d8ae-c830-4047-bc9c-a9ad9b093e33
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (1128LL - 48LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fab9cdc3-89c6-4329-bc2a-afa0f2eb8b39
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (1176LL - 49LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b3178f58-6cb7-4888-8519-70b207c2e6f0
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (1225LL - 50LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 51319f87-66b2-4e7c-bbe4-425972de411e
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (1275LL - 51LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 68ce9bb4-b867-4559-992b-1eecc3d748a6
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (1326LL - 52LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d9775c9f-fb01-4b41-954c-9c8d0d862cb1
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (1378LL - 53LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a48af32-5994-49b1-b56b-47e4b89a0d5e
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (1431LL - 54LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d7d79ffe-2b74-4754-8419-0d4620678ad6
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (1485LL - 55LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a005f529-fb9a-4e09-9665-18f373d6932f
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (1540LL - 56LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 420eaca9-e540-4635-b004-a0a01f618d47
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (1596LL - 57LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7fb51010-fd54-4858-af32-d8b36e6ba0f9
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (1653LL - 58LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8708fb7f-408d-4ef8-b797-abe6e7a5c740
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (1711LL - 59LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c6b821c-d275-4b69-9683-436f5e3379f2
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (1770LL - 60LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ca750023-4457-4f88-9c45-e4fa20cf2811
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (1830LL - 61LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d7078530-6ca7-428a-b9df-dd60d7f63f92
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (1891LL - 62LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0bfe99f0-c613-49fe-8f10-5f18c877fcc5
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (1953LL - 63LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5bbfff01-b112-465b-bd49-f1f03f5eed1f
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (2016LL - 64LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e94186c5-618f-4d2a-b3ac-d4eb5046f245
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (2080LL - 65LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 93181001-97f6-4a72-afeb-82c7a3aa0935
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (2145LL - 66LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 32f87600-719b-4e25-b5a9-6f7cb9ba8650
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (2211LL - 67LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 831f9e89-edc5-405d-9370-472bff3ef21e
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (2278LL - 68LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b147110f-fbee-483f-98f9-eba47fcad3c1
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (2346LL - 69LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9ace7ebb-ff8c-4ce4-8d48-be503197cd80
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (2415LL - 70LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a8ba2f2-13fc-4a27-a3e5-d2a00a085743
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (2485LL - 71LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ccbb17bf-5c67-4a87-97dc-da5e0c52fcb4
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (2556LL - 72LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e33c9e53-641e-4296-9850-799e8066a64b
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (2628LL - 73LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a14e6767-e6b1-4782-a0fe-246d38bf14c5
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (2701LL - 74LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3fde99bb-f823-4b54-8644-e03c394a859f
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (2775LL - 75LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c903d55d-300e-4dee-a0ab-61dc99043777
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (2850LL - 76LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5399de26-2299-4657-9aff-7eeb887da33f
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (2926LL - 77LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 943b3fdb-2cb3-48fe-bf05-d7f09595ee5c
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (3003LL - 78LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 90d43a64-2a64-40a7-95d4-65cb4fb8899f
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (3081LL - 79LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5993ccac-4956-469a-b0df-9d3a7eef44fa
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (3160LL - 80LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a99341ec-dd26-4e9d-a841-e296757706ba
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (3240LL - 81LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9c2a8db0-17d1-4293-9015-e1a1b6693bdd
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (3321LL - 82LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0033c60d-f645-45b2-8efe-73a70bd1e83d
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (3403LL - 83LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 977cbfe6-9f5d-4375-817d-2c88863d9ce1
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (3486LL - 84LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 95ab86fc-baec-48f6-a028-89230d25d214
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (3570LL - 85LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b87d9a0f-8cf0-4503-9d8e-36c018e8c71d
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (3655LL - 86LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0efee2f4-c34f-44ea-ae89-8863dbe6c6ec
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (3741LL - 87LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5453f7d9-4c26-440a-8d17-50919e5e5ef6
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (3828LL - 88LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c7180ccf-5f79-41ee-85fb-1ca394099268
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (3916LL - 89LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 701255fb-a623-4c93-8874-c336cde40f26
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (4005LL - 90LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f0741d3c-f5dc-4d7e-b99a-8a2ca7787507
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (4095LL - 91LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ca8bca3-5bc1-4c98-9ecd-d28603aec4d2
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (4186LL - 92LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 614867b7-15b4-468f-85d9-308c40f29cb8
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (4278LL - 93LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d21fec63-493d-448e-924b-9ac6222190dc
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (4371LL - 94LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e0724ac6-b869-4a44-82dd-a58a825a3376
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (4465LL - 95LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 30147768-cd41-48e1-8ccf-acd281e802e2
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (4560LL - 96LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b6a3d805-010e-4a49-8b83-1350b372fec4
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (4656LL - 97LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8c05166a-6c0c-48a0-bbe5-4905a9b961f0
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (4753LL - 98LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0f26f83c-958d-4dc3-b42c-041e788feb36
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (4851LL - 99LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 78d1bfa1-7f65-444f-8945-5a38e0a3588b
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (4950LL - 100LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0fefcdcd-196e-4b5d-b32d-2d80aa8a96a8
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (5050LL - 101LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1deb775a-0954-47ca-a167-cc1277253989
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (5151LL - 102LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f8a1c5b-ff99-419c-88ce-e0cb86c12086
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (5253LL - 103LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7b0dba30-1bca-4ff7-bd45-3d36263c9261
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (5356LL - 104LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c10c070-6f35-4cc3-90e0-27874f25a354
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (5460LL - 105LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e2a9c74b-8a29-44e6-975c-0becc7b45e56
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (5565LL - 106LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 949f888b-bc0f-42b4-a8e9-1a2faf158b8c
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (5671LL - 107LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a4c712d-ec85-49a6-928c-67291b3fff3b
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (5778LL - 108LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b98e31f5-f628-4e18-8ce5-e3b4779a2b77
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (5886LL - 109LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3cac6b9d-a247-4d09-b348-ce15becc2d5d
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (5995LL - 110LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 06332de7-8f25-4abb-b5b4-8fedc0cbe2da
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (6105LL - 111LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ae43d6a2-c335-448f-b7b7-567207967870
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (6216LL - 112LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 704176ed-a8dc-4765-9324-dcc560405938
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (6328LL - 113LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ff16079d-4b0b-4bc5-92ba-666813294ca1
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (6441LL - 114LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 734932e8-a9fb-4fde-8b3c-66460b2051d9
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (6555LL - 115LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 618755a2-1ba1-4b68-ad83-6fa497f3ca12
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (6670LL - 116LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2307814f-bd56-4cd4-81ec-30b27c444617
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (6786LL - 117LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 667abf40-00e6-4742-acad-50c4666c1094
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (6903LL - 118LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cebcbe99-2dfc-489c-ba35-448e3f1bae9c
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (7021LL - 119LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 12c762f1-0d30-4fbb-9730-ef7b3201888a
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (7140LL - 120LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 774d1e06-ec79-4af8-b3f1-c9e8fa327e68
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (7260LL - 121LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6b0c3553-177b-4643-91d0-305f443b8672
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (7381LL - 122LL * c) + x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e56abc3-cab6-47e3-b374-ad39f4c620ed
    creation_time: 2023-01-27T15:25:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/ps3-ll_valuebound100.c: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
      data_model: 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/ps3-ll_valuebound100.c
    file_hash: 544518f16c995eb36950e2b23195c44efaa0ec21905798c152f246cf5cd9bc9b
    line: 27
    column: 11
    function: main
  loop_invariant:
    string: (7503LL - 123LL * c) + x >= 0LL
    type: assertion
    format: C
