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/test29_false-unreach-call_true-termination.c
programSHA a3f28e224781fd5d9b8ef9ac65a16e90a58c193eef248ce5ed03064fdc005dcf
witnessName results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.test29_false-unreach-call_true-termination.c.files/witness.graphml
witnessSHA cd73fc3133f63fd2ac23ec8491c4c956278db2851deec1e6ab9a2f7a6c7aea5a

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/cd73fc3133f63fd2ac23ec8491c4c956278db2851deec1e6ab9a2f7a6c7aea5a.json

Key Value
architecture 32bit
creationtime 2017-11-30T15:09 CET (sv-comp)
producer 2LS
program-sha256 a3f28e224781fd5d9b8ef9ac65a16e90a58c193eef248ce5ed03064fdc005dcf
programfile ../../sv-benchmarks/c/ldv-regression/test29_false-unreach-call_true-termination.c
programhash 2aa6c4430411ceeb023b25a4c3a2c7228d94ed35
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/cd73fc3133f63fd2ac23ec8491c4c956278db2851deec1e6ab9a2f7a6c7aea5a.graphml
witness-sha256 cd73fc3133f63fd2ac23ec8491c4c956278db2851deec1e6ab9a2f7a6c7aea5a
witness-size 4338
witness-type violation_witness

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

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

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test29_false-unreach-call_true-termination.c, a3f28e224781fd5d9b8ef9ac65a16e90a58c193eef248ce5ed03064fdc005dcf
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/a3f28e224781fd5d9b8ef9ac65a16e90a58c193eef248ce5ed03064fdc005dcf.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 (a3f28e224781fd5d9b8ef9ac65a16e90a58c193eef248ce5ed03064fdc005dcf, sv-benchmarks/c/ldv-regression/test29_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test29_false-unreach-call_true-termination.c, a3f28e224781fd5d9b8ef9ac65a16e90a58c193eef248ce5ed03064fdc005dcf
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/a3f28e224781fd5d9b8ef9ac65a16e90a58c193eef248ce5ed03064fdc005dcf.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 (a3f28e224781fd5d9b8ef9ac65a16e90a58c193eef248ce5ed03064fdc005dcf, sv-benchmarks/c/ldv-regression/test29_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test29_false-unreach-call_true-termination.c, a3f28e224781fd5d9b8ef9ac65a16e90a58c193eef248ce5ed03064fdc005dcf
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/a3f28e224781fd5d9b8ef9ac65a16e90a58c193eef248ce5ed03064fdc005dcf.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 (a3f28e224781fd5d9b8ef9ac65a16e90a58c193eef248ce5ed03064fdc005dcf, sv-benchmarks/c/ldv-regression/test29_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test29_false-unreach-call_true-termination.c, a3f28e224781fd5d9b8ef9ac65a16e90a58c193eef248ce5ed03064fdc005dcf
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/a3f28e224781fd5d9b8ef9ac65a16e90a58c193eef248ce5ed03064fdc005dcf.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 (a3f28e224781fd5d9b8ef9ac65a16e90a58c193eef248ce5ed03064fdc005dcf, sv-benchmarks/c/ldv-regression/test29_false-unreach-call_true-termination.c).

Found 20 witnesses for program sv-benchmarks/c/ldv-regression/test29_false-unreach-call_true-termination.c, a3f28e224781fd5d9b8ef9ac65a16e90a58c193eef248ce5ed03064fdc005dcf
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/a3f28e224781fd5d9b8ef9ac65a16e90a58c193eef248ce5ed03064fdc005dcf.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 31bfa22 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 19:18:25
Download 95aac9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 4 2019-12-03T23:23 CET (comp)
Download 9597c50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T21:53:04+01:00 Download a1732af
Download e53e811 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T21:45:55+01:00 Download 778d4fa
Download 73decaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T21:09:00+01:00 Download 31bfa22
Download 4d08a54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:44:40+01:00 Download 337b278
Download d8cff04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T01:51:13+01:00 Download d1e094d
Download dd0f01c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T00:26:29+01:00 Download 30882d3
Download c2fbde6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T00:06:01+01:00 Download d140f39
Download 8a3513a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T21:17:49+01:00 Download ccd8aa6
Download c148073 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-06T02:39:27+01:00 Download 1bed9c6
Download c0460ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-04T02:58:10+01:00 Download 95aac9c
Download 395dbd9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-03T08:57:51+01:00 Download ce5b22c
Download 4ae4dc3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-03T08:07:09+01:00 Download d3490b3
Download d3490b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 6 2019-11-30T06:56:11+01:00
Download d1e094d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 6 2019-12-07T16:37:43+01:00
Download 778d4fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 6 2019-12-01T09:36:32+01:00
Download ee8b32e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:54:45+01:00 Download 311d581
Download c314e66 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-05T19:34:02+01:00 Download b520410
Download 59408a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:02 CET (comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c0730df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T13:34 CET (sv-comp)
Download 98c3b7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T02:10:43
Download 5cc137f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 5 2018-12-07T09:34 CET (sv-comp)
Download 3e2f5f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 6 2018-12-10T18:34:32+01:00
Download 1fc5f0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-08T02:09:11+01:00
Download 6432cf5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-10T20:38:01+01:00 Download 3e2f5f4
Download 32918af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:53:23+01:00 Download 1e4034f
Download 088db07 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:36:08+01:00 Download 945a28e
Download c1510bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:21:38+01:00 Download 6d0edb2
Download f8322e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T18:20:53+01:00 Download fe4877b
Download e03f571 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T23:42:04+01:00 Download c0730df
Download 2872a1e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T22:10:17+01:00 Download 98c3b7b
Download c84c5ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T07:45:41+01:00 Download 1fc5f0f
Download aa991c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T03:50:36+01:00 Download 09954d7
Download f201275 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-07T09:14:41+01:00 Download 1ba3851
Download 55114e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-07T01:20:11+01:00 Download df2b2b2
Download f627764 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:48:43+01:00 Download fe8b607
Download 5c20200 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:19:39+01:00 Download 3e5bfde
Download 7921411 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:08:21+01:00 Download 55eee6a
Download fe8b607 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-05T20:05:25+01:00
Download 45bcf2b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T05:03:05+01:00 Download 06d8ca7
Download 4e59f0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T10:17:52+01:00 Download c401cef
Download ec834a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:40:28+01:00 Download cd73fc3
Download 8c30e62 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T04:40 CET (sv-comp)
Download 02b27eb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T12:07 CET (sv-comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c038919 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 6 2017-12-02T20:35Z
Download d9164ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T18:36 CET (sv-comp)
Download 1ba3851 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness PredatorHP 4 2017-12-01T20:30 CET (sv-comp)
Download bb66d0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 3 2017-12-01T21:08 CET (sv-comp)
Download eb763cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 6 2017-12-02T19:52Z
Download 7c065e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 5 2017-12-01T15:24:17.074666
Download af77582 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 5 2017-12-01T08:56:12.230018
Download c598e98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-12-01T16:01 CET (sv-comp)
Download 0233171 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-11-30T18:29 CET (sv-comp)
Download 2fe40e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 6 2017-12-02T23:13:36+01:00
Download 2d2bd95 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-11-30T17:00:37+01:00
Download b40833d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 11 2017-11-30T15:51:21+01:00
Download 6085ef8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 4 2017-12-01T00:56:19+01:00
Download fae5db3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 5 2017-12-01T22:45:47+01:00
Download f4c2c10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 5 2017-12-01T02:35 CET (sv-comp)
Download 514646b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 6 2017-12-02T13:05Z
Download cd73fc3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 4 2017-11-30T15:09 CET (sv-comp)
Download 392e746 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T00:06:26.133754
Download 8782f34 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T09:11:48.125581
Download 19b4a90 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 6 2017-12-01T18:42 CET (sv-comp)
Download dc8872b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2017-12-01T14:41 CET (sv-comp)

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

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

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

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