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_2_false-unreach-call_true-no-overflow.BV.c.cil.c |
programSHA | a593916f94b54e1cc09623f46c714caa1630271c998eeafebcc853bbd93200f1 |
witnessName | results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c.files/witness.graphml |
witnessSHA | 71e2ec91b7b39f0d1884dca2f433f83932975b1d681229081f02aca66fb32df2 |
Key | Value |
architecture | 32bit |
creationtime | 2017-11-30T19:18:25+01:00 |
producer | CPAchecker 1.6.1-svn 26758M |
program-sha256 | a593916f94b54e1cc09623f46c714caa1630271c998eeafebcc853bbd93200f1 |
programfile | ../../sv-benchmarks/c/bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c |
programhash | 0bf79c30a8b941af2e2e52ff71757957757c98e5 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/71e2ec91b7b39f0d1884dca2f433f83932975b1d681229081f02aca66fb32df2.graphml |
witness-sha256 | 71e2ec91b7b39f0d1884dca2f433f83932975b1d681229081f02aca66fb32df2 |
witness-size | 119818 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c, a593916f94b54e1cc09623f46c714caa1630271c998eeafebcc853bbd93200f1
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/a593916f94b54e1cc09623f46c714caa1630271c998eeafebcc853bbd93200f1.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_2_false-unreach-call_true-no-overflow.BV.c.cil.c, a593916f94b54e1cc09623f46c714caa1630271c998eeafebcc853bbd93200f1
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/a593916f94b54e1cc09623f46c714caa1630271c998eeafebcc853bbd93200f1.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_2_false-unreach-call_true-no-overflow.BV.c.cil.c, a593916f94b54e1cc09623f46c714caa1630271c998eeafebcc853bbd93200f1
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/a593916f94b54e1cc09623f46c714caa1630271c998eeafebcc853bbd93200f1.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_2_false-unreach-call_true-no-overflow.BV.c.cil.c, a593916f94b54e1cc09623f46c714caa1630271c998eeafebcc853bbd93200f1
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/a593916f94b54e1cc09623f46c714caa1630271c998eeafebcc853bbd93200f1.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 15 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c, a593916f94b54e1cc09623f46c714caa1630271c998eeafebcc853bbd93200f1
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/a593916f94b54e1cc09623f46c714caa1630271c998eeafebcc853bbd93200f1.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
17ea7cb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 6 | 2019-12-01 08:19:05 | ||
672bdf4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Pinaka | 14 | 2019-12-03T21:49 CET (comp) | ||
40d8cb2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 16 | 2019-12-11T21:53:25+01:00 | 5015de4 | |
e9752a1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 16 | 2019-12-11T21:48:17+01:00 | 2f4145c | |
5e8ac5d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 38 | 2019-12-11T21:09:16+01:00 | 17ea7cb | |
16525c4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 16 | 2019-12-08T00:26:40+01:00 | 215f9b9 | |
93cad40 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 16 | 2019-12-07T21:17:43+01:00 | e3c5773 | |
aff3b90 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 20 | 2019-12-06T02:40:44+01:00 | 16dc699 | |
3ba7dbd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 17 | 2019-12-04T02:58:13+01:00 | 672bdf4 | |
795c2f9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 16 | 2019-12-03T08:10:32+01:00 | 85d83a4 | |
85d83a4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.9 | 16 | 2019-11-30T09:41:23+01:00 | ||
5015de4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 16 | 2019-11-30T21:14:58+01:00 | ||
165aa68 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.9 | 48 | 2019-12-11T20:54:24+01:00 | e1703dd | |
63f8c1e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.9 | 48 | 2019-12-05T20:21:54+01:00 | 7412f52 | |
3473e1b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.9 | 48 | 2019-12-05T19:34:23+01:00 | dc35988 |
Found 19 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c, a593916f94b54e1cc09623f46c714caa1630271c998eeafebcc853bbd93200f1
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/a593916f94b54e1cc09623f46c714caa1630271c998eeafebcc853bbd93200f1.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1026c50 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T20:42 CET (sv-comp) | ||
fdc8cc0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 13 | 2018-12-08T14:20:17 | ||
b413536 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 98 | 2018-12-06T23:09 CET (sv-comp) | ||
87091e4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 112 | 2018-12-10T17:40:03+01:00 | ||
b53f0ab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 143 | 2018-12-07T09:17:36+01:00 | ||
462f364 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 126 | 2018-12-10T20:36:55+01:00 | 87091e4 | |
3f4f695 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 125 | 2018-12-09T20:53:27+01:00 | fa22880 | |
e82a9b4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 125 | 2018-12-09T20:34:30+01:00 | 7fab83d | |
6586b27 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 132 | 2018-12-09T18:20:47+01:00 | 18ebb83 | |
540606d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 126 | 2018-12-08T23:42:20+01:00 | 1026c50 | |
7690703 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 126 | 2018-12-08T22:10:43+01:00 | fdc8cc0 | |
69bfd8c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 159 | 2018-12-08T08:44:35+01:00 | b53f0ab | |
699dbbe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 153 | 2018-12-08T05:02:52+01:00 | 54b1763 | |
51f9637 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 163 | 2018-12-07T17:44:24+01:00 | b413536 | |
b9b6827 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 153 | 2018-12-06T10:17:29+01:00 | 6812d0a | |
08d780b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 159 | 2018-12-06T09:47:56+01:00 | 44a0e02 | |
f67b16e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 169 | 2018-12-06T09:18:27+01:00 | 1b604ea | |
44a0e02 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 143 | 2018-12-05T13:51:29+01:00 | ||
f1a9bfc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 48 | 2018-12-06T09:40:31+01:00 | 3011e28 |
Found 13 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c, a593916f94b54e1cc09623f46c714caa1630271c998eeafebcc853bbd93200f1
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/a593916f94b54e1cc09623f46c714caa1630271c998eeafebcc853bbd93200f1.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
dce6ee2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 120 | 2017-12-02T19:17Z | ||
83c7c52 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-01T23:09 CET (sv-comp) | ||
dea5444 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 14 | 2017-12-01T19:47:58.703687 | ||
318b6d0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 13 | 2017-12-01T08:05:47.163465 | ||
f015e43 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 25 | 2017-12-01T01:14 CET (sv-comp) | ||
ba7c0f0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn | 112 | 2017-12-02T19:14:52+01:00 | ||
9d3f33b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 108 | 2017-12-01T01:27:35+01:00 | ||
71e2ec9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 120 | 2017-11-30T19:18:25+01:00 | ||
417ccee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 82 | 2017-12-01T01:16:14+01:00 | ||
ee56b1d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 56 | 2017-12-02T02:01:31+01:00 | ||
5dc1163 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 111 | 2017-11-30T13:43 CET (sv-comp) | ||
a4c6601 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 120 | 2017-12-02T01:46Z | ||
27c8dbf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 84 | 2017-11-30T15:51 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c, a593916f94b54e1cc09623f46c714caa1630271c998eeafebcc853bbd93200f1
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/a593916f94b54e1cc09623f46c714caa1630271c998eeafebcc853bbd93200f1.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |