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/ldv-regression/nested_structure_true-unreach-call_true-termination.i |
programSHA | b31d089693b52880edcacf5055f3fcbc2ef49eead1ffc9b6b044a38d2dcfabe3 |
witnessName | results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.nested_structure_true-unreach-call_true-termination.i.files/witness.graphml |
witnessSHA | c9d5ded5628bbf586d6bc02a6d27bd4e4a428ad54e8df1912dca006de6e06376 |
Key | Value |
architecture | 32bit |
creationtime | 2017-11-30T20:27:08+01:00 |
producer | CPAchecker 1.6.1-svn 26725 |
program-sha256 | b31d089693b52880edcacf5055f3fcbc2ef49eead1ffc9b6b044a38d2dcfabe3 |
programfile | ../../sv-benchmarks/c/ldv-regression/nested_structure_true-unreach-call_true-termination.i |
programhash | 18fe7e200a4359dbcae87626cdb43abcf2bc6326 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/c9d5ded5628bbf586d6bc02a6d27bd4e4a428ad54e8df1912dca006de6e06376.graphml |
witness-sha256 | c9d5ded5628bbf586d6bc02a6d27bd4e4a428ad54e8df1912dca006de6e06376 |
witness-size | 4078 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-regression/nested_structure_true-unreach-call_true-termination.i, b31d089693b52880edcacf5055f3fcbc2ef49eead1ffc9b6b044a38d2dcfabe3
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/b31d089693b52880edcacf5055f3fcbc2ef49eead1ffc9b6b044a38d2dcfabe3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-regression/nested_structure_true-unreach-call_true-termination.i, b31d089693b52880edcacf5055f3fcbc2ef49eead1ffc9b6b044a38d2dcfabe3
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/b31d089693b52880edcacf5055f3fcbc2ef49eead1ffc9b6b044a38d2dcfabe3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-regression/nested_structure_true-unreach-call_true-termination.i, b31d089693b52880edcacf5055f3fcbc2ef49eead1ffc9b6b044a38d2dcfabe3
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/b31d089693b52880edcacf5055f3fcbc2ef49eead1ffc9b6b044a38d2dcfabe3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-regression/nested_structure_true-unreach-call_true-termination.i, b31d089693b52880edcacf5055f3fcbc2ef49eead1ffc9b6b044a38d2dcfabe3
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/b31d089693b52880edcacf5055f3fcbc2ef49eead1ffc9b6b044a38d2dcfabe3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-regression/nested_structure_true-unreach-call_true-termination.i, b31d089693b52880edcacf5055f3fcbc2ef49eead1ffc9b6b044a38d2dcfabe3
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/b31d089693b52880edcacf5055f3fcbc2ef49eead1ffc9b6b044a38d2dcfabe3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 24 witnesses for program sv-benchmarks/c/ldv-regression/nested_structure_true-unreach-call_true-termination.i, b31d089693b52880edcacf5055f3fcbc2ef49eead1ffc9b6b044a38d2dcfabe3
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/b31d089693b52880edcacf5055f3fcbc2ef49eead1ffc9b6b044a38d2dcfabe3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
da05e0c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T06:37 CET (sv-comp) | ||
a2f9f64 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T02:25:02 | ||
5799c78 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-07T01:29 CET (sv-comp) | ||
47271b4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 4 | 2018-12-06T12:49:49+01:00 | ||
526b552 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-10T20:06:48+01:00 | 042a5b8 | |
97f56f6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-10T10:31:36+01:00 | 532b75a | |
6429841 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-09T20:14:15+01:00 | 8ab0d97 | |
4d312dc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-09T19:54:04+01:00 | 5ca4c83 | |
1963f46 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-09T17:13:07+01:00 | 6ffaeb3 | |
0845a46 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T22:48:16+01:00 | da05e0c | |
b67507b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T21:29:56+01:00 | a2f9f64 | |
4238e5d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T05:52:58+01:00 | 47271b4 | |
d4cd1de | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T03:38:56+01:00 | 73a6a06 | |
29a2f5f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T02:05:26+01:00 | 532b75a | |
a0f0e40 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-07T17:44:24+01:00 | 30e50f3 | |
a38f09b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-07T16:38:02+01:00 | 5799c78 | |
f85ea0b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-07T08:52:42+01:00 | f075974 | |
f06282e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T09:28:28+01:00 | 36b8670 | |
4b13d96 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T09:01:10+01:00 | a5e3c21 | |
3574108 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T07:50:05+01:00 | e4c5f46 | |
707c152 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T07:18:19+01:00 | c00e833 | |
a5e3c21 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T01:19:56+01:00 | ||
37455e2 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T01:07 CET (sv-comp) | ||
9af648b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T14:46 CET (sv-comp) |
Found 41 witnesses for program sv-benchmarks/c/ldv-regression/nested_structure_true-unreach-call_true-termination.i, b31d089693b52880edcacf5055f3fcbc2ef49eead1ffc9b6b044a38d2dcfabe3
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/b31d089693b52880edcacf5055f3fcbc2ef49eead1ffc9b6b044a38d2dcfabe3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
30e50f3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T23:38 CET (sv-comp) | ||
402d45e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 7 | 2017-12-02T19:54Z | ||
c2f8990 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T15:19 CET (sv-comp) | ||
f075974 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | PredatorHP | 4 | 2017-12-01T20:28 CET (sv-comp) | ||
432cfd2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Map2Check | 3 | 2017-12-01T21:11 CET (sv-comp) | ||
b5f4636 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 6 | 2017-12-02T16:38Z | ||
5f425b2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Forester | 5 | 2017-12-01T18:00 CET (sv-comp) | ||
43e4ffe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T22:46:40.659295 | ||
7fe922f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T08:15:16.898909 | ||
9e612a8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T15:49:42.091454 | ||
5142b41 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T09:48:48.153950 | ||
07b154e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 4 | 2017-12-01T19:54 CET (sv-comp) | ||
51da97d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-03T01:21:06+01:00 | ||
082d71a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-11-30T18:22:43+01:00 | ||
0a3bce0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-03T06:50:51+01:00 | 7083198 | |
b09f832 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-03T04:22:34+01:00 | e9e8306 | |
7a2a571 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-03T03:03:48+01:00 | 405a861 | |
2c408a2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-03T01:50:48+01:00 | 023e48a | |
de2d1ba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-02T20:29:12+01:00 | 1f9feb0 | |
2a995f2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-02T14:21:21+01:00 | 156462a | |
9069648 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-02T08:19:04+01:00 | cad87ce | |
3f6ed4b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-02T00:11:39+01:00 | d4c8050 | |
935f3b9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T22:27:17+01:00 | 094950b | |
22546bb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T22:08:47+01:00 | be60f2c | |
9343b81 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T21:03:59+01:00 | cd8cc81 | |
ee4e10b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T18:33:03+01:00 | 16ac744 | |
56a9680 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T08:14:02+01:00 | 5e3a8f5 | |
5dc1190 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T06:07:01+01:00 | 66a15dc | |
41d68d3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T06:02:38+01:00 | 41b8bb8 | |
fe14d2a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T05:50:23+01:00 | 6f6b8db | |
f1410bd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T05:40:01+01:00 | 560fd82 | |
18a9f1f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T04:48:04+01:00 | 7c51b51 | |
9b18798 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-11-30T23:26:27+01:00 | ||
fe08adc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 8 | 2017-11-30T18:25:27+01:00 | ||
c9d5ded | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 4 | 2017-11-30T20:27:08+01:00 | ||
1987a0d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 4 | 2017-12-02T12:22:21+01:00 | ||
2fef3ef | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 5 | 2017-11-30T12:38 CET (sv-comp) | ||
50e4626 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 7 | 2017-12-02T01:39Z | ||
3f3245d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 8 | 2017-11-30T14:24 CET (sv-comp) | ||
290896d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 5 | 2017-12-01T19:19 CET (sv-comp) | ||
def3423 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 8 | 2017-12-01T14:48 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-regression/nested_structure_true-unreach-call_true-termination.i, b31d089693b52880edcacf5055f3fcbc2ef49eead1ffc9b6b044a38d2dcfabe3
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/b31d089693b52880edcacf5055f3fcbc2ef49eead1ffc9b6b044a38d2dcfabe3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |