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/signextension2_false-unreach-call_true-termination.c |
programSHA | d163d24a866cf62d7899207800875399feee2331c1b28ee24ee75492ac4a18ea |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-veriabs.2018-12-10_2034.logfiles/sv-comp19_prop-reachsafety.signextension2_false-unreach-call_true-termination.c.files/witness.graphml |
witnessSHA | 7059aeb0f87a1a180a82f6d5965dfb661bc64aa0dd9a5fb8bac8c8997059efcb |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-10T20:34:48+01:00 |
inputwitnesshash | 494708a329c08d4f9caf400e4d685cdff6a1816cce02e434f345362f106aec49 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | d163d24a866cf62d7899207800875399feee2331c1b28ee24ee75492ac4a18ea |
programfile | ../../sv-benchmarks/c/bitvector-regression/signextension2_false-unreach-call_true-termination.c |
programhash | d163d24a866cf62d7899207800875399feee2331c1b28ee24ee75492ac4a18ea |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/7059aeb0f87a1a180a82f6d5965dfb661bc64aa0dd9a5fb8bac8c8997059efcb.graphml |
witness-sha256 | 7059aeb0f87a1a180a82f6d5965dfb661bc64aa0dd9a5fb8bac8c8997059efcb |
witness-size | 5771 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, d163d24a866cf62d7899207800875399feee2331c1b28ee24ee75492ac4a18ea).
Found 0 witnesses for program sv-benchmarks/c/bitvector-regression/signextension2_false-unreach-call_true-termination.c, d163d24a866cf62d7899207800875399feee2331c1b28ee24ee75492ac4a18ea
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/d163d24a866cf62d7899207800875399feee2331c1b28ee24ee75492ac4a18ea.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/signextension2_false-unreach-call_true-termination.c, d163d24a866cf62d7899207800875399feee2331c1b28ee24ee75492ac4a18ea
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/d163d24a866cf62d7899207800875399feee2331c1b28ee24ee75492ac4a18ea.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/signextension2_false-unreach-call_true-termination.c, d163d24a866cf62d7899207800875399feee2331c1b28ee24ee75492ac4a18ea
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/d163d24a866cf62d7899207800875399feee2331c1b28ee24ee75492ac4a18ea.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/signextension2_false-unreach-call_true-termination.c, d163d24a866cf62d7899207800875399feee2331c1b28ee24ee75492ac4a18ea
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/d163d24a866cf62d7899207800875399feee2331c1b28ee24ee75492ac4a18ea.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 20 witnesses for program sv-benchmarks/c/bitvector-regression/signextension2_false-unreach-call_true-termination.c, d163d24a866cf62d7899207800875399feee2331c1b28ee24ee75492ac4a18ea
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/d163d24a866cf62d7899207800875399feee2331c1b28ee24ee75492ac4a18ea.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6a4a72d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-01 12:09:25 | ||
55fb314 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 5 | 2019-12-03T22:55 CET (comp) | ||
14413ee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-11T21:56:46+01:00 | ef68907 | |
a9908cb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-11T21:54:50+01:00 | 769d5b5 | |
e8234e1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-11T21:09:38+01:00 | 6a4a72d | |
f65d274 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-11T20:54:19+01:00 | 0c6390d | |
266740e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-11T20:44:53+01:00 | 8381ed1 | |
6017201 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-08T01:51:19+01:00 | a77fc1d | |
37f2fec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-08T00:26:20+01:00 | bc46332 | |
ce19276 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-07T21:13:53+01:00 | fed4f7c | |
6a76056 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-06T02:39:18+01:00 | a33ba2c | |
6ebe5db | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-05T20:21:31+01:00 | dd4ed44 | |
ce433d9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-04T02:58:25+01:00 | 55fb314 | |
0e1067c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-03T08:57:05+01:00 | 39d0a5e | |
2de3de2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 6 | 2019-12-03T08:03:15+01:00 | 999dd33 | |
999dd33 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 5 | 2019-11-30T14:25:00+01:00 | ||
a77fc1d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 4 | 2019-12-07T22:31:57+01:00 | ||
ef68907 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 5 | 2019-12-01T01:59:50+01:00 | ||
d4a23a1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-05T19:34:20+01:00 | b7fdd19 | |
1de27c5 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:49 CET (comp) |
Found 27 witnesses for program sv-benchmarks/c/bitvector-regression/signextension2_false-unreach-call_true-termination.c, d163d24a866cf62d7899207800875399feee2331c1b28ee24ee75492ac4a18ea
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/d163d24a866cf62d7899207800875399feee2331c1b28ee24ee75492ac4a18ea.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2980414 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T06:33 CET (sv-comp) | ||
bc56392 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T08:40:37 | ||
a2ee536 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 5 | 2018-12-07T13:45 CET (sv-comp) | ||
494708a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 4 | 2018-12-10T18:43:06+01:00 | ||
6e79513 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 5 | 2018-12-07T15:36:40+01:00 | ||
7059aeb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-10T20:34:48+01:00 | 494708a | |
1974999 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-10T10:48:43+01:00 | 343a0ab | |
750a9df | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T20:53:14+01:00 | 3c78a13 | |
e593bba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T20:35:18+01:00 | db52a7a | |
a46f378 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T20:24:04+01:00 | 548fe46 | |
2f548e3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T18:21:13+01:00 | 64cd699 | |
b471f93 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T23:44:51+01:00 | 2980414 | |
38c6399 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T22:08:02+01:00 | bc56392 | |
f8531c7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T09:05:48+01:00 | 6e79513 | |
51dc601 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T04:56:27+01:00 | 2c2e739 | |
fe18988 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T04:05:50+01:00 | 343a0ab | |
5a82b94 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-07T18:47:37+01:00 | 61697a6 | |
714ddbe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-07T17:45:00+01:00 | a2ee536 | |
a7c7e01 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-07T01:21:09+01:00 | 6a28d0f | |
2b22aab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T10:18:32+01:00 | fdf0767 | |
50391f8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:47:55+01:00 | cac7ad8 | |
9ec3f63 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:19:08+01:00 | 986cc34 | |
abf9578 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:12:06+01:00 | 95930e5 | |
cac7ad8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-05T23:29:39+01:00 | ||
43dc05c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T09:42:13+01:00 | e6f3dfb | |
e9f944f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T17:18 CET (sv-comp) | ||
8350780 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T09:20 CET (sv-comp) |
Found 21 witnesses for program sv-benchmarks/c/bitvector-regression/signextension2_false-unreach-call_true-termination.c, d163d24a866cf62d7899207800875399feee2331c1b28ee24ee75492ac4a18ea
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/d163d24a866cf62d7899207800875399feee2331c1b28ee24ee75492ac4a18ea.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a22ac06 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | skink | 3 | 2017-12-01T22:43 CET (sv-comp) | ||
9b2912c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 6 | 2017-12-02T20:26Z | ||
a1a0d03 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T13:00 CET (sv-comp) | ||
32ffd71 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Map2Check | 4 | 2017-12-01T21:20 CET (sv-comp) | ||
4d425b4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 6 | 2017-12-02T18:27Z | ||
2ff1f9f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-01T19:55:04.737894 | ||
4f6b31b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T09:18:44.556544 | ||
53208ef | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 5 | 2017-12-01T19:27 CET (sv-comp) | ||
dbc08cf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 5 | 2017-11-30T21:36 CET (sv-comp) | ||
3c418f7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-03T03:33:24+01:00 | ||
d5e505f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-11-30T12:16:46+01:00 | ||
b58245a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 5 | 2017-11-30T18:54 CET (sv-comp) | ||
8efb7ea | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 6 | 2017-12-02T09:39Z | ||
e6f3dfb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 5 | 2017-11-30T15:11 CET (sv-comp) | ||
16d070c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T23:38:19.787866 | ||
e9e30f9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T14:39:11.289930 | ||
71988a7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 10 | 2017-11-30T13:01:59+01:00 | ||
f349dcf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 4 | 2017-11-30T22:00:22+01:00 | ||
941397d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 4 | 2017-12-02T05:06:49+01:00 | ||
af5bac2 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 5 | 2017-12-01T14:20 CET (sv-comp) | ||
51be98b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 10 | 2017-12-01T15:26 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/bitvector-regression/signextension2_false-unreach-call_true-termination.c, d163d24a866cf62d7899207800875399feee2331c1b28ee24ee75492ac4a18ea
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/d163d24a866cf62d7899207800875399feee2331c1b28ee24ee75492ac4a18ea.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |