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).
Key | Value |
programName | sv-benchmarks/c/recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c |
programSHA | 854f5cf702fca5695c2c3a6e1d68b132758a0182aecb2ec84b6824a5c5c6d184 |
witnessName | results-verified/divine-explicit.2018-12-10_1000.logfiles/sv-comp19_prop-reachsafety.afterrec_2calls_false-unreach-call_true-termination.c.files/witness.graphml |
witnessSHA | ce730df4687ed5610713f636cbb040194f123e93b7530b0485450ed9d3e459e0 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-07T04:02 CET (sv-comp) |
memorymodel | precise |
producer | DIVINE 4 |
programfile | ../../sv-benchmarks/c/recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c |
programhash | 7757e3f263599cd02799bfad01adb3bcaa895e82 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/ce730df4687ed5610713f636cbb040194f123e93b7530b0485450ed9d3e459e0.graphml |
witness-sha256 | ce730df4687ed5610713f636cbb040194f123e93b7530b0485450ed9d3e459e0 |
witness-size | 3692 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c, 854f5cf702fca5695c2c3a6e1d68b132758a0182aecb2ec84b6824a5c5c6d184
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/854f5cf702fca5695c2c3a6e1d68b132758a0182aecb2ec84b6824a5c5c6d184.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c, 854f5cf702fca5695c2c3a6e1d68b132758a0182aecb2ec84b6824a5c5c6d184
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/854f5cf702fca5695c2c3a6e1d68b132758a0182aecb2ec84b6824a5c5c6d184.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c, 854f5cf702fca5695c2c3a6e1d68b132758a0182aecb2ec84b6824a5c5c6d184
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/854f5cf702fca5695c2c3a6e1d68b132758a0182aecb2ec84b6824a5c5c6d184.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c, 854f5cf702fca5695c2c3a6e1d68b132758a0182aecb2ec84b6824a5c5c6d184
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/854f5cf702fca5695c2c3a6e1d68b132758a0182aecb2ec84b6824a5c5c6d184.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 18 witnesses for program sv-benchmarks/c/recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c, 854f5cf702fca5695c2c3a6e1d68b132758a0182aecb2ec84b6824a5c5c6d184
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/854f5cf702fca5695c2c3a6e1d68b132758a0182aecb2ec84b6824a5c5c6d184.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a22ef19 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-01 16:52:05 | ||
5ec862a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 5 | 2019-12-04T00:55 CET (comp) | ||
fd86129 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-11T21:56:23+01:00 | 320adcd | |
fcbfb0b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-11T21:09:00+01:00 | a22ef19 | |
5729df6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-11T20:55:21+01:00 | 7cd30e2 | |
6ee736c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-11T20:44:29+01:00 | 8a0fdb7 | |
982dc2e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-06T02:39:08+01:00 | 496a1a9 | |
97ca714 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-03T08:10:04+01:00 | 2401033 | |
2401033 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 5 | 2019-11-30T04:33:12+01:00 | ||
320adcd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 5 | 2019-12-01T06:58:58+01:00 | ||
814c858 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-11T21:47:39+01:00 | 7369443 | |
80dcf4b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-08T01:51:19+01:00 | 0f92c21 | |
df7ee16 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-08T00:26:01+01:00 | 53720cd | |
3a18cd2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-07T21:14:12+01:00 | 913c7b9 | |
bcee182 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-05T20:20:13+01:00 | 92ff6d0 | |
a3d2e85 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-04T02:58:14+01:00 | 5ec862a | |
7615bdb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-03T08:57:55+01:00 | ff4530d | |
3fd3050 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:31 CET (comp) |
Found 25 witnesses for program sv-benchmarks/c/recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c, 854f5cf702fca5695c2c3a6e1d68b132758a0182aecb2ec84b6824a5c5c6d184
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/854f5cf702fca5695c2c3a6e1d68b132758a0182aecb2ec84b6824a5c5c6d184.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
43b646a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T07:36 CET (sv-comp) | ||
d4ba2c4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 4 | 2018-12-08T13:41:11 | ||
a34e13e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 5 | 2018-12-07T10:33 CET (sv-comp) | ||
1ffa9b3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 7 | 2018-12-07T04:03:14+01:00 | ||
c083269 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T18:10:37+01:00 | 49efa96 | |
fa9022c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T23:43:38+01:00 | 43b646a | |
702db20 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T22:11:38+01:00 | d4ba2c4 | |
5455fcb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T04:52:12+01:00 | 65ecff7 | |
3026e82 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-07T01:23:24+01:00 | e6b8522 | |
992ffed | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T10:19:02+01:00 | 9e434c9 | |
f1548e2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:48:31+01:00 | e64b76f | |
e64b76f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-05T16:17:43+01:00 | ||
0d943af | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-10T20:38:06+01:00 | 7e46762 | |
bf9961d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-10T10:48:53+01:00 | ce730df | |
ff34e94 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T21:23:37+01:00 | 4912d1d | |
028297d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T20:53:07+01:00 | 3881049 | |
fe4f3c0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T20:38:23+01:00 | 3e4bbaa | |
795642d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T20:28:36+01:00 | c2e0786 | |
ade1f57 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T08:09:48+01:00 | 1ffa9b3 | |
c49cb55 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T04:02:33+01:00 | ce730df | |
bc761ce | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-07T17:43:44+01:00 | a34e13e | |
bfc80f2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:19:33+01:00 | d993a81 | |
2197e9d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:18:33+01:00 | dc6b76c | |
ffc9f91 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T08:10 CET (sv-comp) | ||
f6942e4 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T06:39 CET (sv-comp) |
Found 18 witnesses for program sv-benchmarks/c/recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c, 854f5cf702fca5695c2c3a6e1d68b132758a0182aecb2ec84b6824a5c5c6d184
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/854f5cf702fca5695c2c3a6e1d68b132758a0182aecb2ec84b6824a5c5c6d184.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4912d1d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | VIAP | 5 | 2017-12-03T03:54 CET (sv-comp) | ||
04a6085 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 7 | 2017-12-03T03:04Z | ||
2004dce | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T12:34 CET (sv-comp) | ||
a40a4aa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Map2Check | 4 | 2017-12-01T20:51 CET (sv-comp) | ||
c9171b1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 7 | 2017-12-02T18:03Z | ||
7ca6845 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-01T20:31:37.665400 | ||
b6b42e6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T13:01:35.341291 | ||
977190c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 5 | 2017-12-01T20:57 CET (sv-comp) | ||
9e9f438 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 5 | 2017-12-01T04:08 CET (sv-comp) | ||
234806a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-11-30T17:00:23+01:00 | ||
0ed07ec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 7 | 2017-11-30T19:57:43+01:00 | ||
cdddcfb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 5 | 2017-11-30T19:47:02+01:00 | ||
b5fe89e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 6 | 2017-12-02T08:25:33+01:00 | ||
f986733 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 5 | 2017-11-30T12:05 CET (sv-comp) | ||
7083390 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 7 | 2017-12-02T00:44Z | ||
1af231c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T22:00:44.256290 | ||
2b83e4f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T12:31:12.794798 | ||
2888817 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 5 | 2017-12-01T14:18 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c, 854f5cf702fca5695c2c3a6e1d68b132758a0182aecb2ec84b6824a5c5c6d184
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/854f5cf702fca5695c2c3a6e1d68b132758a0182aecb2ec84b6824a5c5c6d184.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |