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/implicitunsignedconversion_false-unreach-call_true-termination.c |
programSHA | e95689a8b9c07109c1f6aa77e8cd9c3c9f6e13517a57b1039e9d63d7d6faffe9 |
witnessName | results-verified/pinaka.2018-12-06_2014.logfiles/sv-comp19_prop-termination.implicitunsignedconversion_false-unreach-call_true-termination.c.files/witness.graphml |
witnessSHA | 48a0a2bd8a590f642fe37de426ec191b92e3249bca6012b89195ad2e8ffbc0c0 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-06T20:27 CET (sv-comp) |
producer | Pinaka |
program-sha256 | e95689a8b9c07109c1f6aa77e8cd9c3c9f6e13517a57b1039e9d63d7d6faffe9 |
programfile | ../../sv-benchmarks/c/bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c |
programhash | e95689a8b9c07109c1f6aa77e8cd9c3c9f6e13517a57b1039e9d63d7d6faffe9 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(F end) ) |
witness-file | witnessFileByHash/48a0a2bd8a590f642fe37de426ec191b92e3249bca6012b89195ad2e8ffbc0c0.graphml |
witness-sha256 | 48a0a2bd8a590f642fe37de426ec191b92e3249bca6012b89195ad2e8ffbc0c0 |
witness-size | 3211 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, e95689a8b9c07109c1f6aa77e8cd9c3c9f6e13517a57b1039e9d63d7d6faffe9).
Found 0 witnesses for program sv-benchmarks/c/bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c, e95689a8b9c07109c1f6aa77e8cd9c3c9f6e13517a57b1039e9d63d7d6faffe9
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/e95689a8b9c07109c1f6aa77e8cd9c3c9f6e13517a57b1039e9d63d7d6faffe9.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/implicitunsignedconversion_false-unreach-call_true-termination.c, e95689a8b9c07109c1f6aa77e8cd9c3c9f6e13517a57b1039e9d63d7d6faffe9
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/e95689a8b9c07109c1f6aa77e8cd9c3c9f6e13517a57b1039e9d63d7d6faffe9.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/implicitunsignedconversion_false-unreach-call_true-termination.c, e95689a8b9c07109c1f6aa77e8cd9c3c9f6e13517a57b1039e9d63d7d6faffe9
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/e95689a8b9c07109c1f6aa77e8cd9c3c9f6e13517a57b1039e9d63d7d6faffe9.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/implicitunsignedconversion_false-unreach-call_true-termination.c, e95689a8b9c07109c1f6aa77e8cd9c3c9f6e13517a57b1039e9d63d7d6faffe9
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/e95689a8b9c07109c1f6aa77e8cd9c3c9f6e13517a57b1039e9d63d7d6faffe9.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/implicitunsignedconversion_false-unreach-call_true-termination.c, e95689a8b9c07109c1f6aa77e8cd9c3c9f6e13517a57b1039e9d63d7d6faffe9
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/e95689a8b9c07109c1f6aa77e8cd9c3c9f6e13517a57b1039e9d63d7d6faffe9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f594eea | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-01 10:38:35 | ||
9ef470e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 4 | 2019-12-04T00:42 CET (comp) | ||
cd74327 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-11T22:00:53+01:00 | 333cbf6 | |
f55f143 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-11T21:44:16+01:00 | 117df91 | |
8731152 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-11T21:09:02+01:00 | f594eea | |
ffac6c6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-11T20:54:47+01:00 | 43c32e3 | |
a97dedd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-11T20:44:26+01:00 | 65d9bfb | |
c0ce597 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-08T01:51:30+01:00 | 50af6b5 | |
52867fa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-08T00:27:03+01:00 | b0c55d4 | |
093ca2c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-07T21:16:13+01:00 | c864b50 | |
43c9858 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-06T02:38:55+01:00 | 3e3bd0d | |
d3e7fae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-05T20:20:40+01:00 | 3fb0b07 | |
b9cbc51 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-04T02:58:17+01:00 | 9ef470e | |
54d1268 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-03T08:57:46+01:00 | 9b5d78c | |
a6907c3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 5 | 2019-12-03T08:09:56+01:00 | 82f5273 | |
82f5273 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 4 | 2019-11-30T09:54:19+01:00 | ||
50af6b5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 4 | 2019-12-07T22:26:36+01:00 | ||
333cbf6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 4 | 2019-12-01T04:15:37+01:00 | ||
c4d3178 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-05T19:34:29+01:00 | ad4d076 | |
c251da2 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:59 CET (comp) |
Found 27 witnesses for program sv-benchmarks/c/bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c, e95689a8b9c07109c1f6aa77e8cd9c3c9f6e13517a57b1039e9d63d7d6faffe9
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/e95689a8b9c07109c1f6aa77e8cd9c3c9f6e13517a57b1039e9d63d7d6faffe9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f025e76 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T08:47 CET (sv-comp) | ||
ab0aecd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T04:57:20 | ||
558a7a2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 4 | 2018-12-06T22:42 CET (sv-comp) | ||
c17f580 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 4 | 2018-12-10T17:31:00+01:00 | ||
fd3452b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 4 | 2018-12-07T10:09:23+01:00 | ||
69afd57 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-10T20:37:09+01:00 | c17f580 | |
385176b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-10T10:48:50+01:00 | 11afae2 | |
c88981b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-09T20:53:21+01:00 | 2641dda | |
0762fd0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-09T20:35:19+01:00 | 1a54b64 | |
abda882 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-09T20:25:20+01:00 | f20cb21 | |
1d7d4b8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-09T18:21:49+01:00 | 6cb88ca | |
55094ab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T23:41:57+01:00 | f025e76 | |
eb86df0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T22:09:27+01:00 | ab0aecd | |
b5fe4d8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T08:46:09+01:00 | fd3452b | |
ed373cf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T05:04:01+01:00 | 6b74356 | |
543e93d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T03:29:24+01:00 | 11afae2 | |
8da1313 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-07T18:25:34+01:00 | 6cf3db4 | |
a7d2c9d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-07T17:44:25+01:00 | 558a7a2 | |
1a378ab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-07T01:20:26+01:00 | 5fdca40 | |
f015b7b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T10:18:50+01:00 | 75736e3 | |
ff834e3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:49:03+01:00 | bbf5b4c | |
19c4395 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:16:55+01:00 | dd85edf | |
6197c9a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:11:34+01:00 | e7ea1cd | |
bbf5b4c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T01:39:56+01:00 | ||
03d6947 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T09:40:42+01:00 | 04e7e6b | |
71cb00c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T01:52 CET (sv-comp) | ||
48a0a2b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-06T20:27 CET (sv-comp) |
Found 21 witnesses for program sv-benchmarks/c/bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c, e95689a8b9c07109c1f6aa77e8cd9c3c9f6e13517a57b1039e9d63d7d6faffe9
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/e95689a8b9c07109c1f6aa77e8cd9c3c9f6e13517a57b1039e9d63d7d6faffe9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
aa89e7b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | skink | 3 | 2017-12-01T22:47 CET (sv-comp) | ||
0aec07d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 4 | 2017-12-03T02:47Z | ||
7a1db1f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T12:50 CET (sv-comp) | ||
0968286 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Map2Check | 3 | 2017-12-01T19:54 CET (sv-comp) | ||
12cc81f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 4 | 2017-12-02T07:25Z | ||
31501ee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-01T22:12:21.497579 | ||
bffdec6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T08:20:05.386265 | ||
2633acf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 4 | 2017-12-01T15:52 CET (sv-comp) | ||
c3e2fcc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 4 | 2017-12-01T00:36 CET (sv-comp) | ||
74e3c31 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-02T18:19:59+01:00 | ||
eb4b7e8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-11-30T22:23:55+01:00 | ||
43a5a75 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 4 | 2017-11-30T16:00 CET (sv-comp) | ||
a99a627 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 4 | 2017-12-02T06:18Z | ||
04e7e6b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 4 | 2017-11-30T15:26 CET (sv-comp) | ||
274a93a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T19:57:40.228739 | ||
192e72b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T10:15:05.798273 | ||
42dc982 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 6 | 2017-12-01T02:39:17+01:00 | ||
3e9c193 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 4 | 2017-11-30T14:54:57+01:00 | ||
b4491d0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker (unknown version) | 4 | 2017-12-02T01:20:49+01:00 | ||
df4dfee | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 4 | 2017-12-01T14:21 CET (sv-comp) | ||
c6305ce | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 7 | 2017-12-01T13:27 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c, e95689a8b9c07109c1f6aa77e8cd9c3c9f6e13517a57b1039e9d63d7d6faffe9
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/e95689a8b9c07109c1f6aa77e8cd9c3c9f6e13517a57b1039e9d63d7d6faffe9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |