Witness Inspection

A description of this web service can be found in the CAV paper "Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses" (more material).

View and Validate the Witness

Input Given to this Service about the Witness (URL Query)

Key Value
programName sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca_true-termination.c.i
programSHA 31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d
witnessName results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-termination.cll_search-alloca_true-termination.c.i.files/witness.graphml
witnessSHA e7680ec7a1c04aa9892fc74d72f1936d510f94ac4527162deebb048db3b889bf

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/e7680ec7a1c04aa9892fc74d72f1936d510f94ac4527162deebb048db3b889bf.json

Key Value
architecture 32bit
creationtime 2018-12-06T03:38:21.999385
producer DepthK v3.0
programfile /tmp/vcloud-vcloud-master/worker/working_dir_898da508-9fc2-4b37-a11a-997565a38b19/sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca_true-termination.c.i
programhash 816332e473b7c1902e38959216cb986fa8f0c468
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/e7680ec7a1c04aa9892fc74d72f1936d510f94ac4527162deebb048db3b889bf.graphml
witness-sha256 e7680ec7a1c04aa9892fc74d72f1936d510f94ac4527162deebb048db3b889bf
witness-size 3494
witness-type correctness_witness

Available Results for the Program from Witness Store SV-COMP '24

Trying to find witnesses for program (31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d, sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca_true-termination.c.i).

Found 26 witnesses for program sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca_true-termination.c.i, 31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7bfafec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:48:01+01:00
Download 500bc52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2023-12-03T04:25:18Z
Download 911d0d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 14 2023-12-02T17:21:26Z
Download 4021ecd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T11:17:29Z
Download 087ea23 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 39 2023-12-01T00:59:37Z
Download b43ba43 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-19T14:41:11+01:00 Download c8c25fd
Download 29ff86a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-19T03:34:24+01:00 Download 88cb4f6
Download 18c8847 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-17T06:04:12+01:00 Download b791057
Download 60c64a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-04T11:25:49+01:00 Download 911d0d4
Download e132f59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-04T02:13:35+01:00 Download 568f639
Download c1f7327 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-03T18:29:38+01:00 Download 7bfafec
Download f300f25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-03T09:54:17+01:00 Download 500bc52
Download dae0953 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-01T03:43:18+01:00 Download 087ea23
Download cf25f42 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-30T23:54:24+01:00 Download 279e73a
Download ca24f43 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-30T11:32:10+01:00 Download f8e8d42
Download f8e8d42 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-30T06:10:14+01:00
Download 7f77b0d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-29T18:10:33+01:00 Download 4021ecd
Download 1011a75 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-29T08:21:00+01:00 Download 947f93f
Download 568f639 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 8 2023-12-03T23:10:46+01:00
Download b791057 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 8 2023-12-17T02:51:27+01:00
Download 88cb4f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 8 2023-12-19T00:00:26+01:00
Download 947f93f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 14 2023-11-29T03:31:56Z
Download 279e73a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 44 2023-11-30T22:08:18+01:00
Download fff5cc8 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: d21124ba-2ab7-4cf6-8df6-22e969190935 creation_time: '2023-12-02T18:21:26+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_44ca1fbc-ead8-4041-9174-4fa20894e15f/sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca-1.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_44ca1fbc-ead8-4041-9174-4fa20894e15f/sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca-1.i : 31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] correctness_witness CPAchecker 2.3 9 2023-12-04T11:56:51+01:00
Download c2c5aad Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 6a05905c-2a84-4a86-8177-0bc06f298d7b creation_time: '2023-11-29T04:31:56+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5de716c2-e758-4aa1-a3db-b6f7a5c8fa1e/sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca-1.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5de716c2-e758-4aa1-a3db-b6f7a5c8fa1e/sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca-1.i : 31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5de716c2-e758-4aa1-a3db-b6f7a5c8fa1e/sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca-1.i file_hash: 31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d line: 552 column: 0 function: init_cll value: ((((n <= 2147483647) && (i == 1)) && (n <= 2147483647)) || (((n <= 2147483647) && (2 <= i)) && (n <= 2147483647))) format: c_expression correctness_witness CPAchecker 2.3 9 2023-11-29T07:49:17+01:00
Download c91b345 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: 36c8dc9c-f736-4d91-ad4a-4f51aae4ff13 creation_time: 2023-12-01T00:59:38Z producer: name: Goblint version: tags/svcomp24-0-gc2e9465a7 command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--sets'' ''ana.specification'' ''../../sv-benchmarks/c/properties/no-overflow.prp'' ''--sets'' ''exp.architecture'' ''64bit'' ''../../sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca-1.i''' task: input_files: - ../../sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca-1.i input_file_hashes: ../../sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca-1.i: 31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca-1.i file_hash: 31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d line: 552 column: 6 function: init_cll value: (0LL - (long long )i) + (long long )n >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca-1.i file_hash: 31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d line: 552 column: 6 function: init_cll value: n != 0 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca-1.i file_hash: 31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d line: 552 column: 6 function: init_cll value: (curr == next_node && ((((((((8 <= n && 8 <= i) && (-16LL + (long long )i) + (long long )n >= 0LL) || ((7 <= n && (-14LL + (long long )i) + (long long )n >= 0LL) && i == 7)) || ((6 <= n && (-12LL + (long long )i) + (long long )n >= 0LL) && i == 6)) || ((5 <= n && (-10LL + (long long )i) + (long long )n >= 0LL) && i == 5)) || ((4 <= n && (-8LL + (long long )i) + (long long )n >= 0LL) && i == 4)) || ((3 <= n && (-6LL + (long long )i) + (long long )n >= 0LL) && i == 3)) || ((2 <= n && (-4LL + (long long )i) + (long long )n >= 0LL) && i == 2))) || ((((1 <= n && (-2LL + (long long )i) + (long long )n >= 0LL) && 1 == i) && head == curr) && i == 1) format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca-1.i file_hash: 31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d line: 564 column: 9 function: search value: i <= 2147483646 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca-1.i file_hash: 31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d line: 564 column: 9 function: search value: ((((((((((((((((((((((((1 <= i && i != 0) || (0 <= i && head == curr)) || (1 <= i && i != 0)) || (1 <= i && i != 0)) || (1 <= i && i != 0)) || (1 <= i && i != 0)) || (1 <= i && i != 0)) || (1 <= i && i != 0)) || (1 <= i && i != 0)) || (1 <= i && i != 0)) || (1 <= i && i != 0)) || (1 <= i && i != 0)) || (1 <= i && i != 0)) || (1 <= i && i != 0)) || (1 <= i && i != 0)) || (1 <= i && i != 0)) || (1 <= i && i != 0)) || (1 <= i && i != 0)) || (1 <= i && i != 0)) || (1 <= i && i != 0)) || (1 <= i && i != 0)) || (1 <= i && i != 0)) || (1 <= i && i != 0)) || (1 <= i && i != 0)) || (1 <= i && i != 0) format: c_expression correctness_witness CPAchecker 2.3 12 2023-12-01T05:23:48+01:00

Available Results for the Program from Witness Store SV-COMP '23

Trying to find witnesses for program (31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d, sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca_true-termination.c.i).

Found 23 witnesses for program sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca_true-termination.c.i, 31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fca2a32 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-11T01:47:43+01:00
Download 9853a23 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2022-12-09T12:11:48Z
Download faba8f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 13 2022-12-14T02:19:09Z
Download aeb1c45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T12:09:01Z
Download dd24e11 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp23-0-g4f5dcf38f) 71 2022-12-10T07:15:14Z
Download 9b5ea84 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T11:09:21+01:00 Download faba8f7
Download 6ec6bb7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T07:39:26+01:00 Download ccc93c7
Download b8f4a15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T03:51:09+01:00 Download aeb1c45
Download 7828a0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T02:35:34+01:00 Download 235bf52
Download 2197f9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T00:06:21+01:00 Download 015b7e4
Download 053a439 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T22:50:43+01:00 Download fca2a32
Download 78eb8be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T22:26:20+01:00 Download dd24e11
Download e44b48c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T18:33:20+01:00 Download 9fa6e6e
Download 819067b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T17:38:47+01:00 Download 9853a23
Download 3201b7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T11:01:50+01:00 Download 5c5380a
Download 0510439 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T00:32:25+01:00 Download b4848db
Download 0f095fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-27T23:09:12+01:00 Download aaaea33
Download 5c5380a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2022-12-10T16:43:38+01:00
Download 235bf52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 8 2022-12-11T20:32:05+01:00
Download b4848db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 8 2022-12-25T10:41:06+01:00
Download 9fa6e6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 8 2022-12-10T02:31:38+01:00
Download ccc93c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 13 2022-12-13T14:39:47Z
Download aaaea33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 44 2022-12-07T22:43:22+01:00

Available Results for the Program from Witness Store SV-COMP '22

Trying to find witnesses for program (31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d, sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca_true-termination.c.i).

Found 1 witnesses for program sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca_true-termination.c.i, 31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ee4527e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2021-12-10T17:29:12

Available Results for the Program from Witness Store SV-COMP '21

Trying to find witnesses for program (31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d, sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca_true-termination.c.i).

Found 2 witnesses for program sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca_true-termination.c.i, 31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fe832da Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-11T19:12:45
Download 0c1fd20 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-08T22:35:21

Available Results for the Program from Witness Store SV-COMP '20

Trying to find witnesses for program (31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d, sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca_true-termination.c.i).

Found 0 witnesses for program sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca_true-termination.c.i, 31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '19

Trying to find witnesses for program (31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d, sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca_true-termination.c.i).

Found 0 witnesses for program sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca_true-termination.c.i, 31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '18

Trying to find witnesses for program (31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d, sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca_true-termination.c.i).

Found 1 witnesses for program sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca_true-termination.c.i, 31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 59f1687 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 10 2017-12-01T17:19 CET (sv-comp)

Available Results for the Program from Witness Store SV-COMP '17

Trying to find witnesses for program (31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d, sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca_true-termination.c.i).

Found 0 witnesses for program sv-benchmarks/c/termination-memory-linkedlists/cll_search-alloca_true-termination.c.i, 31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/31928742423b43f372aa35821d3230472c2503cd43386360fe33079ee4c7d30d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness