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/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i |
programSHA | 50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded |
witnessName | results-verified/esbmc-kind.2018-12-06_1103.logfiles/sv-comp19_prop-nooverflow.byte_add_2_true-unreach-call_true-no-overflow_true-termination.i.files/witness.graphml |
witnessSHA | c985b3c3afcc7df5400990b76f8c1fbfd2121706608d50fb28fe5ef717e3a8ed |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-07T14:36:46.118811 |
producer | ESBMC 6.0.0 kind |
programfile | ../../sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i |
programhash | 889a23428ce9b0e3800ffce916f37e53fe302b49 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! overflow) ) |
witness-file | witnessFileByHash/c985b3c3afcc7df5400990b76f8c1fbfd2121706608d50fb28fe5ef717e3a8ed.graphml |
witness-sha256 | c985b3c3afcc7df5400990b76f8c1fbfd2121706608d50fb28fe5ef717e3a8ed |
witness-size | 3412 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i, 50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i, 50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i, 50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i, 50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 18 witnesses for program sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i, 50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
feefa4c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2019-12-04T01:15 CET (comp) | ||
9d6f92a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.9 | 19 | 2019-11-29T21:58:51+01:00 | ||
25e0127 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 19 | 2019-12-01T16:39:16+01:00 | ||
ae8f47c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2019-12-04T01:29 CET (comp) | ||
9f5be4c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-12-11T20:17:24+01:00 | a5b36e1 | |
1eb4f39 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-12-11T20:12:23+01:00 | 7104cf2 | |
a3516ce | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-12-11T20:02:31+01:00 | 2ed7ff1 | |
dbd300c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-12-08T00:50:18+01:00 | 2db3b0e | |
39bbc8e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-12-06T02:18:32+01:00 | e2dcef8 | |
b62e807 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-12-05T19:13:05+01:00 | dd2ead7 | |
e5b08d2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-12-05T19:02:53+01:00 | 8c261d4 | |
0b0b86d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-12-04T02:08:00+01:00 | ae8f47c | |
ffefcc9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-11-30T19:57:48+01:00 | a25723e | |
3ecc7e8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-11-30T16:54:39+01:00 | 0f3f55c | |
0f3f55c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 19 | 2019-11-30T10:48:48+01:00 | ||
2db3b0e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8 | 27 | 2019-12-07T21:49:28+01:00 | ||
a5b36e1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 19 | 2019-12-01T17:48:11+01:00 | ||
09e6b4a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:06 CET (comp) |
Found 25 witnesses for program sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i, 50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
bcca920 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T09:32 CET (sv-comp) | ||
2b827b8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T11:03:46 | ||
9049fbe | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2018-12-07T01:01 CET (sv-comp) | ||
4e8019f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 19 | 2018-12-08T04:03:36+01:00 | ||
574f083 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 19 | 2018-12-05T12:29:54+01:00 | ||
af78ca1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T01:12 CET (sv-comp) | ||
26b717f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T10:51:56 | ||
8f46e84 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-07T06:55 CET (sv-comp) | ||
3455ba3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7 | 27 | 2018-12-10T17:06:12+01:00 | ||
0b5b508 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 27 | 2018-12-06T21:20:59+01:00 | ||
b8e6860 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 26 | 2018-12-10T20:09:01+01:00 | 3455ba3 | |
e0dbee7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-08T23:08:25+01:00 | af78ca1 | |
05fb405 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-08T21:33:32+01:00 | 26b717f | |
3e334f4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-08T06:49:14+01:00 | 0b5b508 | |
3726776 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-08T03:21:16+01:00 | 14abb00 | |
c305d90 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-08T03:02:23+01:00 | 23dd3ce | |
a909dab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-07T16:38:25+01:00 | 8f46e84 | |
d5b610c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-06T09:28:24+01:00 | 8533456 | |
9a854fa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-06T08:45:57+01:00 | 7062387 | |
5a48aec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-06T08:28:51+01:00 | 3f6044c | |
4edbd3d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-06T08:09:50+01:00 | 882dddc | |
7062387 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 19 | 2018-12-06T07:28:58+01:00 | ||
2c340c4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-06T07:04:41+01:00 | ee0b3dd | |
8970312 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T10:23 CET (sv-comp) | ||
df0d427 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T11:15 CET (sv-comp) |
Found 34 witnesses for program sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i, 50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8f6ec85 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 39 | 2017-12-03T07:43Z | ||
6c13dab | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 1 | 2017-12-03T04:46 CET (sv-comp) | ||
c88a5cb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Map2Check | 9 | 2017-12-02T01:20 CET (sv-comp) | ||
a427007 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 40 | 2017-12-03T10:20Z | ||
eabec73 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T18:29:16.072787 | ||
da8a60d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-02T06:53:32.459426 | ||
0f1358f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | ESBMC 3.1 | 23 | 2017-12-01T14:09 CET (sv-comp) | ||
fffa5b8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-12-01T11:32:42+01:00 | ||
cffd005 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CBMC | 69 | 2017-12-01T12:00 CET (sv-comp) | ||
24a05a8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 39 | 2017-12-03T10:20Z | ||
dcc265e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | 2LS | 43 | 2017-12-01T10:54 CET (sv-comp) | ||
fa1c472 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 31 | 2017-12-02T06:55:43+01:00 | ||
6d4c7c0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-01T22:58 CET (sv-comp) | ||
2de0d08 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Map2Check | 9 | 2017-12-01T19:55 CET (sv-comp) | ||
00e2e71 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T02:19:25.722328 | ||
c108a64 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T12:25:56.294463 | ||
3b4cc0e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T18:03:04.967687 | ||
2ea1adc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T08:34:45.188833 | ||
8bf9d7e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 28 | 2017-12-01T16:58 CET (sv-comp) | ||
6cae503 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 22 | 2017-12-02T22:17:19+01:00 | ||
be59d9f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-11-30T17:17:56+01:00 | ||
b95f667 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 23 | 2017-12-03T04:06:13+01:00 | 3f6015c | |
d96129b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-12-02T20:34:17+01:00 | 9b70bbf | |
88bb77d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-12-02T07:38:26+01:00 | f69be3d | |
4bebae0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-12-01T22:31:15+01:00 | 0e35b5b | |
0945bae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-12-01T22:15:16+01:00 | 9d171ab | |
13b573a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-12-01T08:13:04+01:00 | ef38cfa | |
9782737 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-12-01T06:40:10+01:00 | 7958a1a | |
8f91086 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-12-01T04:59:30+01:00 | 7d54775 | |
429b91d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-12-01T04:49:07+01:00 | e56ee3b | |
1049f27 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-11-30T18:43:45+01:00 | ||
62c42cf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 63 | 2017-11-30T20:10 CET (sv-comp) | ||
5d1c5de | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 121 | 2017-11-30T20:26 CET (sv-comp) | ||
0da4658 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 63 | 2017-12-01T16:38 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i, 50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |