- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: be438c1e-96a1-49bf-9759-2e3934ee3ae7
    creation_time: 2023-01-27T15:25:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= r
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c98a2eb6-71fe-420b-bd14-d854d2cb9dd9
    creation_time: 2023-01-27T15:25:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 989fca7e-5ccd-4571-a5b5-c5cbfb596226
    creation_time: 2023-01-27T15:25:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 35081f46-38df-4d9b-9e16-f9f95e1cd178
    creation_time: 2023-01-27T15:25:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: r <= 4294967295LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8aea2db5-4f22-4996-b47e-ff9fcb347972
    creation_time: 2023-01-27T15:25:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0b494e95-87be-4d11-baa8-73ac85294788
    creation_time: 2023-01-27T15:25:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: (0LL - (long long )B) + d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ce67666c-6507-41f1-87f6-0066ecf26789
    creation_time: 2023-01-27T15:25:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: ((-8589934590LL + 4LL * (long long )B) - 3LL * d) + 8589934590LL * p >=
      0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8355b43f-74ff-41e0-9b6d-c29822f0baa6
    creation_time: 2023-01-27T15:25:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: ((-4294967295LL + (long long )B) - d) + 4294967295LL * p >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 89a09476-b152-4ec6-b08d-30f0cbdd3b80
    creation_time: 2023-01-27T15:25:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: (2LL * (long long )A + (long long )B) - d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2499c166-d7a3-4010-bca9-0649f302787e
    creation_time: 2023-01-27T15:25:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    line: 46
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b4d34a9b-0b27-48df-8e8f-bbd05a6ead1d
    creation_time: 2023-01-27T15:25:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    line: 46
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 38b69c25-dfef-4449-94e1-ec43dc61e86c
    creation_time: 2023-01-27T15:25:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    line: 46
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 13134e7d-d964-4481-9e79-df3ac9ccf1c5
    creation_time: 2023-01-27T15:25:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    line: 46
    column: 11
    function: main
  loop_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
