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/bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c |
programSHA | 600073a24a5bc84a6b24945560a7b3a7e9c32d3f20e85969576f739b974848b5 |
witnessName | results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c.files/witness.graphml |
witnessSHA | d27ce9b309672aef0067a125e0d67a53f77977bb7e96379b729678dca52a72eb |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-02T02:33:35.927202 |
producer | ESBMC 4.6.0 kind |
program-sha256 | 600073a24a5bc84a6b24945560a7b3a7e9c32d3f20e85969576f739b974848b5 |
programfile | ../../sv-benchmarks/c/bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c |
programhash | efb326e7cdb5d466c12dff4e56d538f4a9b94761 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/d27ce9b309672aef0067a125e0d67a53f77977bb7e96379b729678dca52a72eb.graphml |
witness-sha256 | d27ce9b309672aef0067a125e0d67a53f77977bb7e96379b729678dca52a72eb |
witness-size | 3419 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c, 600073a24a5bc84a6b24945560a7b3a7e9c32d3f20e85969576f739b974848b5
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/600073a24a5bc84a6b24945560a7b3a7e9c32d3f20e85969576f739b974848b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c, 600073a24a5bc84a6b24945560a7b3a7e9c32d3f20e85969576f739b974848b5
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/600073a24a5bc84a6b24945560a7b3a7e9c32d3f20e85969576f739b974848b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c, 600073a24a5bc84a6b24945560a7b3a7e9c32d3f20e85969576f739b974848b5
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/600073a24a5bc84a6b24945560a7b3a7e9c32d3f20e85969576f739b974848b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c, 600073a24a5bc84a6b24945560a7b3a7e9c32d3f20e85969576f739b974848b5
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/600073a24a5bc84a6b24945560a7b3a7e9c32d3f20e85969576f739b974848b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 13 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c, 600073a24a5bc84a6b24945560a7b3a7e9c32d3f20e85969576f739b974848b5
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/600073a24a5bc84a6b24945560a7b3a7e9c32d3f20e85969576f739b974848b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9f24d91 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Pinaka | 13 | 2019-12-03T21:44 CET (comp) | ||
ca290e9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 15 | 2019-12-11T21:47:13+01:00 | a7d6fc3 | |
1b4872f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 15 | 2019-12-11T21:46:16+01:00 | 2d40f58 | |
e810c51 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 15 | 2019-12-08T00:26:16+01:00 | 7979040 | |
0fb32ed | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 15 | 2019-12-07T21:15:32+01:00 | 3be8b48 | |
01e4a16 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 16 | 2019-12-04T02:58:18+01:00 | 9f24d91 | |
b487f03 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 15 | 2019-12-03T08:07:54+01:00 | 4affbcf | |
4affbcf | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 15 | 2019-11-30T07:22:56+01:00 | ||
a7d6fc3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 15 | 2019-12-01T01:55:34+01:00 | ||
b231ee5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.9 | 48 | 2019-12-11T20:55:11+01:00 | d6da46b | |
8ad1e07 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.9 | 48 | 2019-12-06T02:42:59+01:00 | 00c8bea | |
212e68d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.9 | 48 | 2019-12-05T20:20:24+01:00 | 61fc0d5 | |
b568365 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.9 | 48 | 2019-12-05T19:34:13+01:00 | 69d91d0 |
Found 14 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c, 600073a24a5bc84a6b24945560a7b3a7e9c32d3f20e85969576f739b974848b5
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/600073a24a5bc84a6b24945560a7b3a7e9c32d3f20e85969576f739b974848b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
96eeb03 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T04:26 CET (sv-comp) | ||
6475aed | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T05:21:36 | ||
0f8a1cf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 48 | 2018-12-06T23:50:24+01:00 | ||
b4058a4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 48 | 2018-12-10T19:51:40+01:00 | ca88b1e | |
f0e5963 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 48 | 2018-12-09T20:28:11+01:00 | 7674d17 | |
13c7e73 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 48 | 2018-12-09T20:06:36+01:00 | ac2554f | |
9ee3cf8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 48 | 2018-12-08T23:17:16+01:00 | 96eeb03 | |
363da6d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 48 | 2018-12-08T21:48:05+01:00 | 6475aed | |
f907d9d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 48 | 2018-12-08T06:04:05+01:00 | 0f8a1cf | |
e2f7735 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 48 | 2018-12-08T03:31:21+01:00 | 107f00d | |
ac7b9d9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 48 | 2018-12-06T09:29:53+01:00 | fc46b5d | |
819a99d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 48 | 2018-12-06T08:54:23+01:00 | de3fd1e | |
de3fd1e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 48 | 2018-12-06T07:53:35+01:00 | ||
08137aa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 48 | 2018-12-06T07:05:37+01:00 | 1b64491 |
Found 21 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c, 600073a24a5bc84a6b24945560a7b3a7e9c32d3f20e85969576f739b974848b5
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/600073a24a5bc84a6b24945560a7b3a7e9c32d3f20e85969576f739b974848b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ea366f5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 47 | 2017-12-02T06:09:41+01:00 | ||
9a61f6d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 98 | 2017-12-02T23:46Z | ||
7176d15 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T18:43 CET (sv-comp) | ||
d27ce9b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T02:33:35.927202 | ||
6a704ee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T16:22:28.537362 | ||
703889e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 52 | 2017-12-02T21:42:01+01:00 | ||
0759bcd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-11-30T21:00:10+01:00 | ||
0b03f9b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 48 | 2017-12-03T06:51:49+01:00 | 806ebfa | |
8c56ab2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 52 | 2017-12-03T04:18:28+01:00 | 9688f3c | |
9d1ed76 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 48 | 2017-12-03T00:43:27+01:00 | 65940d7 | |
7b1a581 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 48 | 2017-12-02T20:12:17+01:00 | c679b7d | |
03c0097 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 48 | 2017-12-02T07:39:44+01:00 | e03982b | |
9792b47 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 48 | 2017-12-01T22:37:45+01:00 | a1a6666 | |
e0a5e8a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 48 | 2017-12-01T08:14:29+01:00 | 5493bc4 | |
8e427f7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 48 | 2017-12-01T06:54:51+01:00 | a22751d | |
92705ee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 48 | 2017-12-01T06:24:29+01:00 | 450dc66 | |
9b182d4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 48 | 2017-12-01T04:58:41+01:00 | c71613d | |
1a9f73c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 48 | 2017-11-30T13:54:40+01:00 | ||
dbff337 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 858 | 2017-12-01T01:08 CET (sv-comp) | ||
3233920 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 98 | 2017-12-02T07:42Z | ||
968790b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 942 | 2017-11-30T12:28 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c, 600073a24a5bc84a6b24945560a7b3a7e9c32d3f20e85969576f739b974848b5
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/600073a24a5bc84a6b24945560a7b3a7e9c32d3f20e85969576f739b974848b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |