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/ldv-regression/test28_false-unreach-call_true-termination.c
programSHA 25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656
witnessName results-validated/cpa-seq-validate-violation-witnesses-pesco.2018-12-08_0739.logfiles/sv-comp19_prop-reachsafety.test28_false-unreach-call_true-termination.c.files/witness.graphml
witnessSHA 69b5b8bcf8d2525970d976af7a05013d126a36c3956460c2884126c4cd59e056

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-08T07:54:49+01:00
inputwitnesshash 121519fb9786d12b1b076b34e2a0a77e78c619277a092635036bea10a81b1268
producer CPAchecker 1.7-svn 29852
program-sha256 25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656
programfile ../../sv-benchmarks/c/ldv-regression/test28_false-unreach-call_true-termination.c
programhash 25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/69b5b8bcf8d2525970d976af7a05013d126a36c3956460c2884126c4cd59e056.graphml
witness-sha256 69b5b8bcf8d2525970d976af7a05013d126a36c3956460c2884126c4cd59e056
witness-size 6257
witness-type violation_witness

This witness was created for this program (cf. table above, 25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656).

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

Trying to find witnesses for program (25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656, sv-benchmarks/c/ldv-regression/test28_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test28_false-unreach-call_true-termination.c, 25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656.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 '23

Trying to find witnesses for program (25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656, sv-benchmarks/c/ldv-regression/test28_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test28_false-unreach-call_true-termination.c, 25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656.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 '22

Trying to find witnesses for program (25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656, sv-benchmarks/c/ldv-regression/test28_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test28_false-unreach-call_true-termination.c, 25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656.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 '21

Trying to find witnesses for program (25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656, sv-benchmarks/c/ldv-regression/test28_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test28_false-unreach-call_true-termination.c, 25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656.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 '20

Trying to find witnesses for program (25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656, sv-benchmarks/c/ldv-regression/test28_false-unreach-call_true-termination.c).

Found 19 witnesses for program sv-benchmarks/c/ldv-regression/test28_false-unreach-call_true-termination.c, 25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a806c1f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 15:43:25
Download 045fd17 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 4 2019-12-04T00:29 CET (comp)
Download b46d945 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 7 2019-12-11T21:56:14+01:00 Download 44d2e1f
Download 89a6a01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T21:43:57+01:00 Download 1063e34
Download 4b8c013 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T21:09:05+01:00 Download a806c1f
Download 4e74a4d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T01:51:45+01:00 Download 8cf1730
Download a9b1e41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 7 2019-12-08T00:27:27+01:00 Download 26c878e
Download 730a8a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 7 2019-12-08T00:07:04+01:00 Download 6a42599
Download ac94afe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 7 2019-12-07T21:12:47+01:00 Download 39f2163
Download 6ae546a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 7 2019-12-05T20:21:43+01:00 Download 064dece
Download f49da07 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 7 2019-12-04T02:58:24+01:00 Download 045fd17
Download 8efe10e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-03T08:02:58+01:00 Download 3f1eb04
Download 3f1eb04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 6 2019-11-29T15:04:43+01:00
Download 8cf1730 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 6 2019-12-07T16:23:09+01:00
Download 1063e34 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 6 2019-12-01T00:40:35+01:00
Download 55eb144 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-06T02:40:48+01:00 Download a25ba1a
Download b525dd5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-05T19:34:03+01:00 Download ed73b8f
Download d166c8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-03T08:56:49+01:00 Download a9bf453
Download f127e1a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:44 CET (comp)

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

Trying to find witnesses for program (25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656, sv-benchmarks/c/ldv-regression/test28_false-unreach-call_true-termination.c).

Found 24 witnesses for program sv-benchmarks/c/ldv-regression/test28_false-unreach-call_true-termination.c, 25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0b160fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-07T21:52 CET (sv-comp)
Download 941814d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T18:59:38
Download ddac955 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 4 2018-12-07T04:44 CET (sv-comp)
Download 17f77e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 6 2018-12-10T17:27:59+01:00
Download 121519f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-08T04:06:27+01:00
Download 65e10ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-10T20:35:23+01:00 Download 17f77e0
Download a4c7255 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:53:16+01:00 Download 04e1e19
Download 1229b42 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:36:41+01:00 Download ce8139c
Download a17dcf9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:31:07+01:00 Download f01ad45
Download 5da229b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T23:43:45+01:00 Download 0b160fe
Download 3b75fbc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T22:10:07+01:00 Download 941814d
Download 69b5b8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T07:54:49+01:00 Download 121519f
Download b6d9caa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T04:55:50+01:00 Download d790f58
Download ab0dd35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-07T18:47:35+01:00 Download cafdd40
Download ab3f9c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-07T17:44:36+01:00 Download ddac955
Download 0459116 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-07T09:14:11+01:00 Download a308c3b
Download e9646dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T10:17:15+01:00 Download 2c910bf
Download ff5d483 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:49:06+01:00 Download 536551f
Download b9bbeab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:08:02+01:00 Download bd4e747
Download 4601a6d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:01:59+01:00 Download 83d93fb
Download 536551f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T03:41:17+01:00
Download a5e5dba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:42:16+01:00 Download 9ae6ef9
Download 3c664a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T08:00 CET (sv-comp)
Download 54dc990 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-06T23:48 CET (sv-comp)

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

Trying to find witnesses for program (25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656, sv-benchmarks/c/ldv-regression/test28_false-unreach-call_true-termination.c).

Found 21 witnesses for program sv-benchmarks/c/ldv-regression/test28_false-unreach-call_true-termination.c, 25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ba4e15b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 5 2017-12-03T04:47Z
Download e2bf368 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T17:21 CET (sv-comp)
Download a308c3b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness PredatorHP 4 2017-12-01T20:33 CET (sv-comp)
Download 7c2f280 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 2 2017-12-01T21:02 CET (sv-comp)
Download 9857359 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 5 2017-12-02T01:45Z
Download 34c30db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T04:20:27.498914
Download d97c6f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T18:23:22.780891
Download 41ad9f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-12-01T18:57 CET (sv-comp)
Download aa2b1d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-11-30T18:40 CET (sv-comp)
Download ab69227 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 6 2017-12-02T23:09:48+01:00
Download 86fc2cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-11-30T15:19:47+01:00
Download ab98218 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 10 2017-12-01T00:00:18+01:00
Download c1f43bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 4 2017-11-30T12:58:52+01:00
Download e476080 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-01T19:55:44+01:00
Download ad3bd3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 5 2017-11-30T23:07 CET (sv-comp)
Download 4f46d04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 5 2017-12-02T00:40Z
Download 9ae6ef9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 4 2017-12-01T01:07 CET (sv-comp)
Download 372eaf6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T19:51:44.785185
Download 4fab4c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T10:42:56.436878
Download 2648b4b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 5 2017-12-01T14:05 CET (sv-comp)
Download 9e1c418 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2017-12-01T15:58 CET (sv-comp)

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

Trying to find witnesses for program (25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656, sv-benchmarks/c/ldv-regression/test28_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test28_false-unreach-call_true-termination.c, 25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/25b5a0090b9ae7194828d2350bbf98509b61e6f16494ee54aaf65615a3630656.json

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