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/eca-rers2012/Problem02_label16_false-unreach-call_false-termination.c |
programSHA | 7ee02f0d7a4caa3d038d1d64c0bcac45ab0b53d4de437fae4864f71831b42c86 |
witnessName | results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.Problem02_label16_false-unreach-call_false-termination.c.files/witness.graphml |
witnessSHA | 8bc32c2360e1eb29aec2f533bf4dbe0ab37edae2c0c328c57c86db1433f3409f |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-02T19:57 CET (sv-comp) |
memorymodel | precise |
producer | Veriabs |
program-sha256 | 7ee02f0d7a4caa3d038d1d64c0bcac45ab0b53d4de437fae4864f71831b42c86 |
programfile | /home/benchexec/ar_abs_temp/Problem02_label16_false_unreach_call_false_termination_c.c |
programhash | b5d27e813284518a11dcc3cc5ae3d66f549ea677 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/8bc32c2360e1eb29aec2f533bf4dbe0ab37edae2c0c328c57c86db1433f3409f.graphml |
witness-sha256 | 8bc32c2360e1eb29aec2f533bf4dbe0ab37edae2c0c328c57c86db1433f3409f |
witness-size | 2727 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label16_false-unreach-call_false-termination.c, 7ee02f0d7a4caa3d038d1d64c0bcac45ab0b53d4de437fae4864f71831b42c86
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/7ee02f0d7a4caa3d038d1d64c0bcac45ab0b53d4de437fae4864f71831b42c86.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label16_false-unreach-call_false-termination.c, 7ee02f0d7a4caa3d038d1d64c0bcac45ab0b53d4de437fae4864f71831b42c86
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/7ee02f0d7a4caa3d038d1d64c0bcac45ab0b53d4de437fae4864f71831b42c86.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label16_false-unreach-call_false-termination.c, 7ee02f0d7a4caa3d038d1d64c0bcac45ab0b53d4de437fae4864f71831b42c86
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/7ee02f0d7a4caa3d038d1d64c0bcac45ab0b53d4de437fae4864f71831b42c86.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label16_false-unreach-call_false-termination.c, 7ee02f0d7a4caa3d038d1d64c0bcac45ab0b53d4de437fae4864f71831b42c86
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/7ee02f0d7a4caa3d038d1d64c0bcac45ab0b53d4de437fae4864f71831b42c86.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 19 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label16_false-unreach-call_false-termination.c, 7ee02f0d7a4caa3d038d1d64c0bcac45ab0b53d4de437fae4864f71831b42c86
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/7ee02f0d7a4caa3d038d1d64c0bcac45ab0b53d4de437fae4864f71831b42c86.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
b6eb64c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-01 20:52:58 | ||
8898ae5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 31 | 2019-12-04T00:16 CET (comp) | ||
c9708fa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 85 | 2019-12-11T21:57:01+01:00 | 817237c | |
7cf7e23 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 81 | 2019-12-11T21:45:05+01:00 | 1493730 | |
4ec1642 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 81 | 2019-12-11T21:09:25+01:00 | b6eb64c | |
54a4ba6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 81 | 2019-12-11T20:54:23+01:00 | 1afd4e7 | |
78287e7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 81 | 2019-12-11T20:44:27+01:00 | fa4744a | |
598d388 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 81 | 2019-12-08T01:51:19+01:00 | 64ee689 | |
5e9e126 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 85 | 2019-12-08T00:26:03+01:00 | 463b008 | |
8b56646 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 85 | 2019-12-07T21:17:47+01:00 | 44090b0 | |
c4bbbfc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 94 | 2019-12-04T02:58:06+01:00 | 8898ae5 | |
bd7efa0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 81 | 2019-12-03T08:09:53+01:00 | ad621c7 | |
ad621c7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 80 | 2019-11-30T02:32:49+01:00 | ||
1493730 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 81 | 2019-12-01T00:41:15+01:00 | ||
a992c40 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-05T20:22:06+01:00 | f06489a | |
ed4df01 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 280 | 2019-12-05T19:35:15+01:00 | e75bf39 | |
efc3e0a | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Symbiotic | 2 | 2019-12-01 20:21:30 | ||
8d9e32b | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 359 | 2019-11-30T13:15:19+01:00 | ||
1eba2b0 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 359 | 2019-12-01T07:06:44+01:00 |
Found 25 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label16_false-unreach-call_false-termination.c, 7ee02f0d7a4caa3d038d1d64c0bcac45ab0b53d4de437fae4864f71831b42c86
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/7ee02f0d7a4caa3d038d1d64c0bcac45ab0b53d4de437fae4864f71831b42c86.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7574a26 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T12:17 CET (sv-comp) | ||
55b4526 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 6 | 2018-12-08T07:46:07 | ||
71f0aef | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 36 | 2018-12-07T06:02 CET (sv-comp) | ||
e103834 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 81 | 2018-12-07T19:06:43+01:00 | ||
ea3adca | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 81 | 2018-12-10T20:34:55+01:00 | 2092113 | |
a9645d3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 85 | 2018-12-09T20:35:26+01:00 | 4490d4c | |
4078094 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 81 | 2018-12-09T18:20:56+01:00 | 726a234 | |
11f67db | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 81 | 2018-12-08T23:44:44+01:00 | 7574a26 | |
ee55dfc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 81 | 2018-12-08T22:11:32+01:00 | 55b4526 | |
53f205d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 81 | 2018-12-08T08:26:56+01:00 | e103834 | |
be30a35 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 81 | 2018-12-08T04:59:41+01:00 | 9514d28 | |
4e70f9b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 81 | 2018-12-08T03:25:40+01:00 | e8b389f | |
5b2d77d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 94 | 2018-12-07T17:26:43+01:00 | 71f0aef | |
e78eaaa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 81 | 2018-12-06T10:17:49+01:00 | d011807 | |
bb1e33b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 81 | 2018-12-06T09:48:05+01:00 | b75f58f | |
e7da222 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 275 | 2018-12-06T09:20:28+01:00 | e3d8a8a | |
b75f58f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 80 | 2018-12-05T13:13:16+01:00 | ||
350a689 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-09T20:53:12+01:00 | d3b0fd4 | |
c2d548e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-09T20:35:53+01:00 | 41f97b6 | |
e72663c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-06T09:43:19+01:00 | 76a9316 | |
7f880c9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 280 | 2018-12-06T09:18:09+01:00 | a78505c | |
45d223b | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 359 | 2018-12-07T19:16:57+01:00 | ||
25410fd | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 356 | 2018-12-08T08:59:48+01:00 | ||
2677f87 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 356 | 2018-12-06T09:48:22+01:00 | ||
4183a6d | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 359 | 2018-12-05T22:57:38+01:00 |
Found 18 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label16_false-unreach-call_false-termination.c, 7ee02f0d7a4caa3d038d1d64c0bcac45ab0b53d4de437fae4864f71831b42c86
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/7ee02f0d7a4caa3d038d1d64c0bcac45ab0b53d4de437fae4864f71831b42c86.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8bc32c2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Veriabs | 3 | 2017-12-02T19:57 CET (sv-comp) | ||
b9b7a09 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 73 | 2017-12-03T05:08Z | ||
dcdbcde | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T12:58 CET (sv-comp) | ||
a77c9c4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 73 | 2017-12-02T11:27Z | ||
7ec4380 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-01T18:28:51.111744 | ||
b6225eb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T10:18:05.793836 | ||
7f3a739 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 10 | 2017-12-01T20:32 CET (sv-comp) | ||
2fdf8cc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 10 | 2017-11-30T21:12 CET (sv-comp) | ||
583687b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 46 | 2017-12-01T02:57:06+01:00 | ||
4f8fcc4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 99 | 2017-11-30T18:28:27+01:00 | ||
91f04f6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 56 | 2017-11-30T16:42:48+01:00 | ||
642aeae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 61 | 2017-12-02T12:35:51+01:00 | ||
db4d0d0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 82 | 2017-11-30T23:13 CET (sv-comp) | ||
793786b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 73 | 2017-12-02T20:49Z | ||
0dc0114 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 39 | 2017-12-01T01:30 CET (sv-comp) | ||
e81a469 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 334 | 2017-12-01T12:55:52+01:00 | ||
a5cc9d6 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 15 | 2017-12-03T11:12Z | ||
19f6925 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 26 | 2017-12-01T13:49 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem02_label16_false-unreach-call_false-termination.c, 7ee02f0d7a4caa3d038d1d64c0bcac45ab0b53d4de437fae4864f71831b42c86
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/7ee02f0d7a4caa3d038d1d64c0bcac45ab0b53d4de437fae4864f71831b42c86.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |