- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f4c8147-89a5-4de4-9bc9-eadbcf3701c3
    creation_time: 2023-01-27T15:24:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
    file_hash: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
    line: 41
    column: 11
    function: main
  loop_invariant:
    string: -9223372036854775807LL <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 633a98e7-1c95-4724-994b-a95b5a28693a
    creation_time: 2023-01-27T15:24:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
    file_hash: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
    line: 41
    column: 11
    function: main
  loop_invariant:
    string: -4611686016279904256LL <= xy
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3363944d-ceb6-43eb-985b-7b7c72bc05a8
    creation_time: 2023-01-27T15:24:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
    file_hash: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
    line: 41
    column: 11
    function: main
  loop_invariant:
    string: -4611686016279904256LL <= yy
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8469ceaa-2f7d-46c2-955b-0bf3b7634e16
    creation_time: 2023-01-27T15:24:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
    file_hash: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
    line: 41
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b9bf66bf-7839-4f14-a16a-6bf53bd5f2a4
    creation_time: 2023-01-27T15:24:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
    file_hash: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
    line: 41
    column: 11
    function: main
  loop_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 279ac6ed-a1fd-4681-9896-05595208537e
    creation_time: 2023-01-27T15:24:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
    file_hash: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
    line: 41
    column: 11
    function: main
  loop_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 74a2e5d1-192b-435a-b1b6-8f4412c4e3fe
    creation_time: 2023-01-27T15:24:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
    file_hash: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
    line: 41
    column: 11
    function: main
  loop_invariant:
    string: c <= 2147483646LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a92ac551-940e-4bbb-b468-916ff485bf87
    creation_time: 2023-01-27T15:24:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
    file_hash: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
    line: 41
    column: 11
    function: main
  loop_invariant:
    string: xy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 041fff19-7073-490b-98e6-11287b5f223c
    creation_time: 2023-01-27T15:24:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
    file_hash: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
    line: 41
    column: 11
    function: main
  loop_invariant:
    string: yy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ddf9c3ea-5523-42ac-a33c-56fc71aa2ef8
    creation_time: 2023-01-27T15:24:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
    file_hash: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
    line: 41
    column: 11
    function: main
  loop_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 335f93e3-7808-4a5d-b612-e5bd03e0acd0
    creation_time: 2023-01-27T15:24:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
    file_hash: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
    line: 47
    column: 15
    function: main
  loop_invariant:
    string: -4611686016279904256LL <= xy
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5cf19178-236c-43d6-926b-e854663d5f15
    creation_time: 2023-01-27T15:24:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
    file_hash: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
    line: 47
    column: 15
    function: main
  loop_invariant:
    string: -4611686016279904256LL <= yy
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b8b89658-bf7a-4af9-ac64-d4ac10b8ab4c
    creation_time: 2023-01-27T15:24:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
    file_hash: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
    line: 47
    column: 15
    function: main
  loop_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c62a4ed-f87b-4b38-a3f0-8923db4d729c
    creation_time: 2023-01-27T15:24:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
    file_hash: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
    line: 47
    column: 15
    function: main
  loop_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4af106a5-4e7c-41e1-aecb-7e019e757691
    creation_time: 2023-01-27T15:24:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
    file_hash: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
    line: 47
    column: 15
    function: main
  loop_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d8fbcd85-72fd-44ee-83bf-8ea8782be016
    creation_time: 2023-01-27T15:24:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
    file_hash: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
    line: 47
    column: 15
    function: main
  loop_invariant:
    string: xy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6b927829-0191-4870-a20f-0eaa64edff81
    creation_time: 2023-01-27T15:24:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
    file_hash: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
    line: 47
    column: 15
    function: main
  loop_invariant:
    string: yy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 21737134-0bbd-4aba-94d9-fb207eac4565
    creation_time: 2023-01-27T15:24:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
    file_hash: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
    line: 47
    column: 15
    function: main
  loop_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0140d40c-4da5-4af9-bf27-0c78595a6a98
    creation_time: 2023-01-27T15:24:55Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
    file_hash: 9439004819e2e34c2ab2e87057bca89732394fc53eb02ecb90192bb8fac7667a
    line: 47
    column: 15
    function: main
  loop_invariant:
    string: b != 0LL
    type: assertion
    format: C
