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-regression/integerpromotion_false-unreach-call_true-termination.c |
programSHA | a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70 |
witnessName | results-verified/depthk.2017-12-01_1515.logfiles/sv-comp18.integerpromotion_false-unreach-call_true-termination.c.files/witness.graphml |
witnessSHA | e6fb6fb6b0cb75f48c9aaba76e2d5a236d775500b772934fea8cde4c18ab2582 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-01T17:11 CET (sv-comp) |
memoryModel | precise |
producer | ESBMC 3.1 |
program-sha256 | a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_a431e82b-6a92-45f6-a0e9-9c3b09a02267/sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c |
programhash | 0ff63897979b5dc3504f5d670d2783900c29ce57 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/e6fb6fb6b0cb75f48c9aaba76e2d5a236d775500b772934fea8cde4c18ab2582.graphml |
witness-sha256 | e6fb6fb6b0cb75f48c9aaba76e2d5a236d775500b772934fea8cde4c18ab2582 |
witness-size | 3965 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c, a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c, a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c, a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c, a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 19 witnesses for program sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c, a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
25868be | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-01 20:02:02 | ||
0fb046d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 4 | 2019-12-04T01:03 CET (comp) | ||
386869a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-11T21:40:41+01:00 | 7637deb | |
8ea7109 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-11T21:09:05+01:00 | 25868be | |
244d1ea | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-11T20:54:29+01:00 | fa89db0 | |
708bd74 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-11T20:44:34+01:00 | fecafa6 | |
72aea48 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-08T01:52:07+01:00 | 6073c9c | |
b3c0622 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-08T00:26:30+01:00 | 5cbd4ab | |
8e588b4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-07T21:16:10+01:00 | edaa94a | |
f3cd0be | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-06T02:41:08+01:00 | d41767a | |
41f4a52 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-05T20:20:30+01:00 | 5446c4a | |
39e0b87 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-04T02:58:17+01:00 | 0fb046d | |
a10f99b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-03T08:56:48+01:00 | 63d126d | |
ddb5029 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-03T08:07:50+01:00 | 96363ac | |
96363ac | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 4 | 2019-11-29T20:35:20+01:00 | ||
6073c9c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 4 | 2019-12-07T19:13:35+01:00 | ||
7637deb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 4 | 2019-12-01T16:13:17+01:00 | ||
2d6fa82 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-05T19:34:00+01:00 | fb9249d | |
e585c25 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:04 CET (comp) |
Found 27 witnesses for program sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c, a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
95d9b28 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T14:09 CET (sv-comp) | ||
20f33a5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 4 | 2018-12-08T12:38:23 | ||
4a178a7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 4 | 2018-12-07T12:22 CET (sv-comp) | ||
2021b34 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 4 | 2018-12-10T18:15:58+01:00 | ||
82f017c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 4 | 2018-12-07T19:22:10+01:00 | ||
416781c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-10T20:35:15+01:00 | 2021b34 | |
7609bf6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-10T10:48:42+01:00 | c477584 | |
4cea92d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-09T20:53:11+01:00 | a50d296 | |
0dc3abc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-09T20:39:57+01:00 | a3a067d | |
ba9b2ba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-09T20:28:45+01:00 | 9366396 | |
1e986ed | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-09T18:14:45+01:00 | e0711be | |
0247c53 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T23:44:41+01:00 | 95d9b28 | |
3f1bac3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T22:08:55+01:00 | 20f33a5 | |
eab0c6d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T08:25:40+01:00 | 82f017c | |
0bff5d9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T05:00:00+01:00 | 7e673b7 | |
4647f35 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T03:41:16+01:00 | c477584 | |
1545040 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-07T18:47:02+01:00 | 4c6fe01 | |
f1d09f1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-07T17:45:45+01:00 | 4a178a7 | |
f6e703b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-07T01:10:10+01:00 | 802258f | |
a1098ea | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T10:17:40+01:00 | 11cd7f2 | |
3a9ba5c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:48:56+01:00 | 9786b54 | |
1b5ffbd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:18:30+01:00 | 944f0e0 | |
f7ebc7d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:06:55+01:00 | 0517650 | |
9786b54 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-05T13:22:21+01:00 | ||
7c6dd49 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T09:42:17+01:00 | c809107 | |
6d0ba0d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T09:22 CET (sv-comp) | ||
aa0f82c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T10:49 CET (sv-comp) |
Found 21 witnesses for program sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c, a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
bb6d7c7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | skink | 3 | 2017-12-01T22:48 CET (sv-comp) | ||
357b73d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 4 | 2017-12-03T03:30Z | ||
053f855 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T15:18 CET (sv-comp) | ||
1f6b63d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Map2Check | 3 | 2017-12-01T21:07 CET (sv-comp) | ||
e1f9b22 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 4 | 2017-12-02T13:00Z | ||
4b0d9f8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T05:18:06.539530 | ||
1e98607 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T10:49:20.316282 | ||
e6fb6fb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 4 | 2017-12-01T17:11 CET (sv-comp) | ||
9e36576 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 4 | 2017-11-30T20:53 CET (sv-comp) | ||
675a924 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-02T23:30:44+01:00 | ||
60a3f18 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T02:25:29+01:00 | ||
413c44f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 6 | 2017-11-30T17:17:00+01:00 | ||
f355732 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 4 | 2017-11-30T19:57:36+01:00 | ||
4a03d10 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 4 | 2017-12-01T23:01:11+01:00 | ||
b9d4892 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 4 | 2017-11-30T18:30 CET (sv-comp) | ||
40255b1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 4 | 2017-12-02T07:20Z | ||
c809107 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 4 | 2017-11-30T14:25 CET (sv-comp) | ||
ac22437 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T01:37:35.579420 | ||
b6d0dfa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T14:23:14.919546 | ||
550c7ed | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 4 | 2017-12-01T14:51 CET (sv-comp) | ||
f3ebe18 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 7 | 2017-12-01T12:54 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c, a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |