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_true-unreach-call_true-termination.c |
programSHA | a985071127513da381b5465a31c7ac9789bd455c2baa7f5de9e112476357fef8 |
witnessName | results-verified/cbmc.2018-12-04_2248.logfiles/sv-comp19_prop-termination.implicitunsignedconversion_true-unreach-call_true-termination.c.files/witness.graphml |
witnessSHA | 8dd89af3e1e19026f16fcf344e164393b51f1b0aac7feace645298b92ce8cbc4 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-06T01:21 CET (sv-comp) |
producer | CBMC |
programfile | ../../sv-benchmarks/c/bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c |
programhash | 30aae13da2995f6cf7e0a5685beedb709cfcbffa |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(F end) ) |
witness-file | witnessFileByHash/8dd89af3e1e19026f16fcf344e164393b51f1b0aac7feace645298b92ce8cbc4.graphml |
witness-sha256 | 8dd89af3e1e19026f16fcf344e164393b51f1b0aac7feace645298b92ce8cbc4 |
witness-size | 3748 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c, a985071127513da381b5465a31c7ac9789bd455c2baa7f5de9e112476357fef8
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/a985071127513da381b5465a31c7ac9789bd455c2baa7f5de9e112476357fef8.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_true-unreach-call_true-termination.c, a985071127513da381b5465a31c7ac9789bd455c2baa7f5de9e112476357fef8
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/a985071127513da381b5465a31c7ac9789bd455c2baa7f5de9e112476357fef8.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_true-unreach-call_true-termination.c, a985071127513da381b5465a31c7ac9789bd455c2baa7f5de9e112476357fef8
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/a985071127513da381b5465a31c7ac9789bd455c2baa7f5de9e112476357fef8.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_true-unreach-call_true-termination.c, a985071127513da381b5465a31c7ac9789bd455c2baa7f5de9e112476357fef8
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/a985071127513da381b5465a31c7ac9789bd455c2baa7f5de9e112476357fef8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 18 witnesses for program sv-benchmarks/c/bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c, a985071127513da381b5465a31c7ac9789bd455c2baa7f5de9e112476357fef8
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/a985071127513da381b5465a31c7ac9789bd455c2baa7f5de9e112476357fef8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
b191983 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:25 CET (comp) | ||
c94674e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-11T20:25:37+01:00 | a4b7505 | |
471c3ec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-11T20:21:09+01:00 | 5a6ed52 | |
ca048ab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-11T20:17:29+01:00 | 4b60645 | |
e19d1f9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-11T20:02:28+01:00 | 21be462 | |
ba62a46 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-08T00:36:34+01:00 | 465cf6c | |
e6a47ca | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-07T23:27:19+01:00 | bbeeac6 | |
dcacbff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-07T19:47:31+01:00 | 01ec375 | |
cdeda46 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-06T02:09:32+01:00 | 55a0dc9 | |
be69455 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-05T19:12:56+01:00 | 268e3b0 | |
ea03867 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-05T19:03:06+01:00 | d97e65e | |
741713a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-12-04T02:07:54+01:00 | b191983 | |
04a183d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-11-30T19:51:12+01:00 | 6b624e7 | |
9e80479 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 4 | 2019-11-30T17:10:07+01:00 | bd53089 | |
bd53089 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 4 | 2019-11-30T04:05:11+01:00 | ||
465cf6c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8 | 4 | 2019-12-07T22:21:19+01:00 | ||
5a6ed52 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 4 | 2019-12-01T00:17:43+01:00 | ||
145fc7d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:20 CET (comp) |
Found 23 witnesses for program sv-benchmarks/c/bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c, a985071127513da381b5465a31c7ac9789bd455c2baa7f5de9e112476357fef8
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/a985071127513da381b5465a31c7ac9789bd455c2baa7f5de9e112476357fef8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
47ff338 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T09:09 CET (sv-comp) | ||
6f31a38 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-07T21:38:10 | ||
898f6b8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-07T10:24 CET (sv-comp) | ||
3acdbda | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 4 | 2018-12-07T21:44:26+01:00 | ||
ee203e9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-10T19:57:56+01:00 | 4be78d8 | |
ad1919e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-10T10:31:00+01:00 | f96ad89 | |
24c7fde | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-09T20:27:14+01:00 | bda4249 | |
7633088 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-09T20:02:02+01:00 | 29328a5 | |
4f5a4b6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-09T19:43:37+01:00 | fe3c276 | |
a0e7c8e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T23:11:32+01:00 | 47ff338 | |
f4e6a0f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T21:44:17+01:00 | 6f31a38 | |
8815697 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T05:33:43+01:00 | 3acdbda | |
a619bf5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T03:12:08+01:00 | f96ad89 | |
0df590a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T02:34:13+01:00 | 03bda4f | |
5904b47 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-07T17:20:58+01:00 | e019ccb | |
fe6c857 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-07T16:38:47+01:00 | 898f6b8 | |
6689bc4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T09:29:03+01:00 | 3126558 | |
d6def51 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T08:45:24+01:00 | 0cd04ff | |
7cb7d46 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T08:30:07+01:00 | 5bbf1ab | |
d650b55 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T07:20:04+01:00 | f68cf73 | |
0cd04ff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-05T15:01:08+01:00 | ||
6747541 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T11:34 CET (sv-comp) | ||
3681cf1 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T06:34 CET (sv-comp) |
Found 34 witnesses for program sv-benchmarks/c/bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c, a985071127513da381b5465a31c7ac9789bd455c2baa7f5de9e112476357fef8
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/a985071127513da381b5465a31c7ac9789bd455c2baa7f5de9e112476357fef8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f451e65 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 4 | 2017-12-02T01:04:48+01:00 | ||
e019ccb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | skink | 3 | 2017-12-01T23:38 CET (sv-comp) | ||
f5913e4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Taipan | 4 | 2017-12-02T19:49Z | ||
0ead29d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2017-12-02T09:28 CET (sv-comp) | ||
c8f2fbc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Kojak | 4 | 2017-12-02T09:01Z | ||
4499ae4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T01:14:33.275526 | ||
8ca998f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T09:39:56.235656 | ||
664db1e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T01:49:01.848016 | ||
f3153b5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-01T18:35:37.790680 | ||
695c45a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 4 | 2017-12-01T15:15 CET (sv-comp) | ||
44edf44 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-02T22:34:30+01:00 | ||
825fcdf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn | 4 | 2017-12-01T07:18:30+01:00 | ||
dbf93f7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-03T06:50:49+01:00 | 84356a7 | |
c97e7fe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-03T04:23:41+01:00 | f673445 | |
3dc09f3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-03T03:00:04+01:00 | f9794cf | |
b331cb9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-02T23:32:00+01:00 | a3a3e32 | |
5323dd0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-02T20:07:24+01:00 | e088656 | |
c310323 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-02T07:28:56+01:00 | 45b4fb2 | |
250344a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-02T00:09:02+01:00 | 842a45a | |
40d322c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T22:29:22+01:00 | e60d800 | |
e39173f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T08:13:50+01:00 | 02d7c6f | |
40fc11a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T06:00:57+01:00 | 225777d | |
90f3d60 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T05:49:17+01:00 | f592901 | |
a2cef31 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T05:48:49+01:00 | 7ca260d | |
e9830a0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T05:07:18+01:00 | 8d9300d | |
8ea283b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T04:42:51+01:00 | 968880c | |
6040459 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-11-30T22:23:14+01:00 | ||
1dd618e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26758M | 6 | 2017-11-30T18:21:22+01:00 | ||
f1d99a7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.6.1-svn 26725 | 4 | 2017-12-01T02:54:47+01:00 | ||
151ec7a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CBMC | 4 | 2017-11-30T23:28 CET (sv-comp) | ||
f89cd12 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Automizer | 4 | 2017-12-02T09:42Z | ||
b940c76 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | 2LS | 7 | 2017-12-01T03:01 CET (sv-comp) | ||
d5e19ba | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 4 | 2017-12-01T14:57 CET (sv-comp) | ||
1ea36c2 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 7 | 2017-12-01T12:19 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c, a985071127513da381b5465a31c7ac9789bd455c2baa7f5de9e112476357fef8
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/a985071127513da381b5465a31c7ac9789bd455c2baa7f5de9e112476357fef8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |