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 | ../../../comp/sv-benchmarks/c/ldv-regression/nested_structure_true-termination.c_true-unreach-call.i |
programSHA | e283df73921888cd5729aff332a4f9efbab42a249ed80055fc64674f2c543bf3 |
witnessName | results-verified/predatorhp.2017-12-01_2024.logfiles/sv-comp18.nested_structure_true-termination.c_true-unreach-call.i.files/witness.graphml |
witnessSHA | 5a450c55967f8949e7a23c9bcdc083974f7745e27a3c1ccb11c292f4dc7d2906 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-01T20:55 CET (sv-comp) |
memorymodel | precise |
producer | PredatorHP |
program-sha256 | e283df73921888cd5729aff332a4f9efbab42a249ed80055fc64674f2c543bf3 |
programfile | ../../sv-benchmarks/c/ldv-regression/nested_structure_true-termination.c_true-unreach-call.i |
programhash | d90463d8e0cbd052bb21c654ec3e821e0001fc9b |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/5a450c55967f8949e7a23c9bcdc083974f7745e27a3c1ccb11c292f4dc7d2906.graphml |
witness-sha256 | 5a450c55967f8949e7a23c9bcdc083974f7745e27a3c1ccb11c292f4dc7d2906 |
witness-size | 3586 |
witness-type | correctness_witness |
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/ldv-regression/nested_structure_true-termination.c_true-unreach-call.i, e283df73921888cd5729aff332a4f9efbab42a249ed80055fc64674f2c543bf3
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/e283df73921888cd5729aff332a4f9efbab42a249ed80055fc64674f2c543bf3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/ldv-regression/nested_structure_true-termination.c_true-unreach-call.i, e283df73921888cd5729aff332a4f9efbab42a249ed80055fc64674f2c543bf3
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/e283df73921888cd5729aff332a4f9efbab42a249ed80055fc64674f2c543bf3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/ldv-regression/nested_structure_true-termination.c_true-unreach-call.i, e283df73921888cd5729aff332a4f9efbab42a249ed80055fc64674f2c543bf3
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/e283df73921888cd5729aff332a4f9efbab42a249ed80055fc64674f2c543bf3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/ldv-regression/nested_structure_true-termination.c_true-unreach-call.i, e283df73921888cd5729aff332a4f9efbab42a249ed80055fc64674f2c543bf3
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/e283df73921888cd5729aff332a4f9efbab42a249ed80055fc64674f2c543bf3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 19 witnesses for program ../../../comp/sv-benchmarks/c/ldv-regression/nested_structure_true-termination.c_true-unreach-call.i, e283df73921888cd5729aff332a4f9efbab42a249ed80055fc64674f2c543bf3
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/e283df73921888cd5729aff332a4f9efbab42a249ed80055fc64674f2c543bf3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9694ce3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2019-12-03T23:27 CET (comp) | ||
22beb01 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-11T20:27:40+01:00 | 85288cc | |
8b1c45c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-11T20:23:27+01:00 | 2b41f28 | |
3592131 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-11T20:14:55+01:00 | 42b6c88 | |
2db1e8b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-11T20:02:43+01:00 | 68364cc | |
7f1ead0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-08T00:37:12+01:00 | f00b542 | |
f090762 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-07T23:46:37+01:00 | ab428d9 | |
0b5f68a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-07T23:41:12+01:00 | 6797ca4 | |
f8dfbd3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-07T19:47:18+01:00 | dc93e98 | |
82df3f5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-06T02:09:22+01:00 | b6512ff | |
6d53827 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-05T19:12:49+01:00 | d711e24 | |
a780cfb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-05T19:02:59+01:00 | ce89bdc | |
79dd0bc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-04T02:08:00+01:00 | 9694ce3 | |
b4931ec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-11-30T19:06:51+01:00 | a2f516d | |
08c6f21 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-11-30T17:06:45+01:00 | e2b534a | |
e2b534a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 4 | 2019-11-30T01:11:41+01:00 | ||
f00b542 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8 | 4 | 2019-12-07T14:08:33+01:00 | ||
42b6c88 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 4 | 2019-12-01T15:47:41+01:00 | ||
c8c7fed | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-03T23:44 CET (comp) |
Found 24 witnesses for program ../../../comp/sv-benchmarks/c/ldv-regression/nested_structure_true-termination.c_true-unreach-call.i, e283df73921888cd5729aff332a4f9efbab42a249ed80055fc64674f2c543bf3
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/e283df73921888cd5729aff332a4f9efbab42a249ed80055fc64674f2c543bf3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
13eab08 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T07:50 CET (sv-comp) | ||
a04470a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T11:48:31 | ||
3eb7523 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-07T10:27 CET (sv-comp) | ||
527d13f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 4 | 2018-12-07T23:00:54+01:00 | ||
c960a76 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-10T19:51:46+01:00 | 81ebb15 | |
7bdd252 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-10T10:31:40+01:00 | 986223e | |
8740556 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-09T20:13:59+01:00 | 985e171 | |
f9f8b82 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-09T20:09:52+01:00 | f58962d | |
207de3a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-09T19:56:31+01:00 | b6d4f75 | |
0809dfb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T23:10:41+01:00 | 13eab08 | |
ddb78f2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T21:28:50+01:00 | a04470a | |
c7d557a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T06:58:04+01:00 | 527d13f | |
d263911 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T03:19:16+01:00 | f969dc2 | |
6c100b9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T02:10:17+01:00 | 986223e | |
df2791a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-07T17:44:39+01:00 | a6209d7 | |
b164650 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-07T16:38:36+01:00 | 3eb7523 | |
6aaca3d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-07T08:41:22+01:00 | 5a450c5 | |
eca1a62 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T09:28:41+01:00 | 2835b7a | |
732e4f0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T08:45:23+01:00 | 55d1000 | |
e71950e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T08:22:24+01:00 | 72830ab | |
89c896b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T08:08:16+01:00 | 6d7f4bf | |
55d1000 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-05T08:06:44+01:00 | ||
1f57ee7 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T05:20 CET (sv-comp) | ||
4101581 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-06T23:50 CET (sv-comp) |
Found 41 witnesses for program ../../../comp/sv-benchmarks/c/ldv-regression/nested_structure_true-termination.c_true-unreach-call.i, e283df73921888cd5729aff332a4f9efbab42a249ed80055fc64674f2c543bf3
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/e283df73921888cd5729aff332a4f9efbab42a249ed80055fc64674f2c543bf3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a6209d7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T23:24 CET (sv-comp) | ||
32facce | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 7 | 2017-12-02T23:34Z | ||
4fbcb06 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T18:19 CET (sv-comp) | ||
5a450c5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | PredatorHP | 4 | 2017-12-01T20:55 CET (sv-comp) | ||
e46d7ff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Map2Check | 3 | 2017-12-01T20:03 CET (sv-comp) | ||
d1e16de | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 7 | 2017-12-02T12:02Z | ||
a430936 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Forester | 4 | 2017-12-01T18:23 CET (sv-comp) | ||
3a0169b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T20:21:34.623823 | ||
935248d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T12:02:10.267114 | ||
9af0c78 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-01T22:45:03.628865 | ||
98a3d3f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T08:03:24.119254 | ||
b8e1042 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 4 | 2017-12-01T18:31 CET (sv-comp) | ||
0540b6e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-02T23:27:31+01:00 | ||
d6c5644 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-01T02:35:08+01:00 | ||
36e0492 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-03T06:59:48+01:00 | bce8406 | |
fa3c5ef | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-03T04:28:35+01:00 | 2a19beb | |
3bff3d9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-03T03:01:51+01:00 | e669947 | |
98a935e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-03T02:02:09+01:00 | aabc03e | |
54386f0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-02T20:33:42+01:00 | 8b09c0b | |
e2bbfd0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-02T15:20:27+01:00 | e4a8d4b | |
9e90162 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-02T07:46:51+01:00 | c99d300 | |
f6041aa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-02T00:04:31+01:00 | 749f1cf | |
a3f2ae1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T22:25:11+01:00 | f98642b | |
59efa6d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T22:13:46+01:00 | ab37b70 | |
875f03c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T21:03:54+01:00 | 0c6271b | |
df3be90 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T18:32:34+01:00 | e3f0c44 | |
d3ebaa8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T08:13:12+01:00 | 56d05c1 | |
dd5a3e8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T07:04:48+01:00 | 196e72d | |
a51b0d2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T05:53:59+01:00 | 11248f9 | |
8f98b64 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T05:23:43+01:00 | bf5916d | |
ce5b4fd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T05:07:11+01:00 | b10e605 | |
1c2af2e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T05:06:38+01:00 | bd27eac | |
9c6a02b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-11-30T11:36:07+01:00 | ||
05aa1ef | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 7 | 2017-11-30T20:42:19+01:00 | ||
104635d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 4 | 2017-11-30T17:39:16+01:00 | ||
4334d5a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 4 | 2017-12-01T21:41:22+01:00 | ||
d57c10e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 4 | 2017-11-30T16:16 CET (sv-comp) | ||
bdf9a10 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 7 | 2017-12-02T16:21Z | ||
c3ebc88 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 8 | 2017-11-30T21:16 CET (sv-comp) | ||
fb61e15 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 4 | 2017-12-01T17:42 CET (sv-comp) | ||
5c70d79 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 8 | 2017-12-01T16:53 CET (sv-comp) |
Found 0 witnesses for program ../../../comp/sv-benchmarks/c/ldv-regression/nested_structure_true-termination.c_true-unreach-call.i, e283df73921888cd5729aff332a4f9efbab42a249ed80055fc64674f2c543bf3
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/e283df73921888cd5729aff332a4f9efbab42a249ed80055fc64674f2c543bf3.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |