Witness Inspection

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).

View and Validate the Witness

Input Given to this Service about the Witness (URL Query)

Key Value
programName sv-benchmarks/c/bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i
programSHA 2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0
witnessName results-verified/cbmc-path.2018-12-04_2245.logfiles/sv-comp19_prop-nooverflow.num_conversion_1_true-unreach-call_true-no-overflow.i.files/witness.graphml
witnessSHA e25e0993430d6ac43670eeec2d6e531dfecb8b1939fba4dcf694be6a498a08e7

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/e25e0993430d6ac43670eeec2d6e531dfecb8b1939fba4dcf694be6a498a08e7.json

Key Value
architecture 32bit
creationtime 2018-12-05T03:50 CET (sv-comp)
producer CBMC
programfile ../../sv-benchmarks/c/bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i
programhash d2a071cc6090a217f48ed180b566a651717a8e39
sourcecodelang C
specification CHECK( init(main()), LTL(G ! overflow) )
witness-file witnessFileByHash/e25e0993430d6ac43670eeec2d6e531dfecb8b1939fba4dcf694be6a498a08e7.graphml
witness-sha256 e25e0993430d6ac43670eeec2d6e531dfecb8b1939fba4dcf694be6a498a08e7
witness-size 19538
witness-type correctness_witness

Available Results for the Program from Witness Store SV-COMP '24

Trying to find witnesses for program (2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0, sv-benchmarks/c/bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i, 2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '23

Trying to find witnesses for program (2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0, sv-benchmarks/c/bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i, 2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '22

Trying to find witnesses for program (2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0, sv-benchmarks/c/bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i, 2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '21

Trying to find witnesses for program (2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0, sv-benchmarks/c/bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i, 2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '20

Trying to find witnesses for program (2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0, sv-benchmarks/c/bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i, 2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '19

Trying to find witnesses for program (2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0, sv-benchmarks/c/bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i).

Found 28 witnesses for program sv-benchmarks/c/bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i, 2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download df68a26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2018-12-08T13:24 CET (sv-comp)
Download 0482621 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness SMACK 1.9.3 3 2018-12-07T20:28:55
Download 713c821 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2018-12-07T04:17 CET (sv-comp)
Download 77f4657 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-08T00:29:25+01:00
Download 91535bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-05T23:14:58+01:00
Download 6b0a587 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T08:53 CET (sv-comp)
Download c5f2767 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-07T20:22:41
Download 010c2ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T12:22 CET (sv-comp)
Download f6fac38 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 6 2018-12-10T19:10:54+01:00
Download fd4a9aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-07T05:20:47+01:00
Download b3f14d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-10T19:41:36+01:00 Download f6fac38
Download 2efbb39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-10T10:31:30+01:00 Download 6d7fc7d
Download 937f7bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:30:18+01:00 Download 26785dc
Download 51a7bc2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:11:10+01:00 Download 4ccb1dd
Download 541d817 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-09T19:41:46+01:00 Download 4774f79
Download 004f6dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T22:58:27+01:00 Download 6b0a587
Download d7e6319 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T21:33:20+01:00 Download c5f2767
Download e8e7c78 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T05:52:26+01:00 Download fd4a9aa
Download de06004 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T02:54:01+01:00 Download d5c50a2
Download 59e980d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-08T02:05:07+01:00 Download 6d7fc7d
Download 3ef43d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T17:44:39+01:00 Download 5c4317b
Download cf146c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-07T16:39:21+01:00 Download 010c2ad
Download df1de84 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:28:31+01:00 Download 52bc88f
Download bf4f114 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:45:34+01:00 Download 4df55de
Download 49543bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T08:28:37+01:00 Download 02680e3
Download 1d97297 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T07:41:31+01:00 Download 992942a
Download 8ac9816 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T07:15:10+01:00 Download f594232
Download 4df55de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-05T13:38:20+01:00

Available Results for the Program from Witness Store SV-COMP '18

Trying to find witnesses for program (2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0, sv-benchmarks/c/bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i).

Found 39 witnesses for program sv-benchmarks/c/bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i, 2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fbc610b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2017-12-03T04:34 CET (sv-comp)
Download 0dcff2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Map2Check 4 2017-12-02T01:08 CET (sv-comp)
Download 3d559e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T17:39:37.538599
Download adcd077 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-02T06:03:21.638592
Download 69ae328 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 3.1 7 2017-12-01T14:11 CET (sv-comp)
Download ee0347c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T11:15:09+01:00
Download 0e46810 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 20 2017-12-01T11:20 CET (sv-comp)
Download fdfdc86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 11 2017-12-01T11:01 CET (sv-comp)
Download 7da0a9e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 16 2017-12-02T04:17:23+01:00
Download 5c4317b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:21 CET (sv-comp)
Download 8e7a065 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 8 2017-12-03T03:16Z
Download fc6507d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T18:52 CET (sv-comp)
Download 0761eed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 4 2017-12-01T21:24 CET (sv-comp)
Download d7e84db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 7 2017-12-02T09:28Z
Download c9885bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T16:07:50.187912
Download 57d5bbf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T08:52:44.342238
Download 1bca0b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 7 2017-12-03T03:26:43+01:00
Download 2bd0429 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T02:15:41+01:00
Download 074136f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T07:05:10+01:00 d6a2355
Download a5c8bec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T04:18:25+01:00 76d3281
Download b08fe24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T01:54:57+01:00 4cbba32
Download fa51565 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-03T01:20:04+01:00 a760b91
Download e9b5be0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T20:23:56+01:00 5924b0a
Download 7faac67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T08:13:58+01:00 d43d116
Download 940a194 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-02T00:09:08+01:00 5b0925c
Download ba92740 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T22:34:43+01:00 e95a288
Download 2b938c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T22:18:49+01:00 e9717f9
Download 799850c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T08:12:58+01:00 112b954
Download 41cb484 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T07:02:39+01:00 b5acc5a
Download a8d354d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T07:02:38+01:00 ab76534
Download b067c62 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T06:52:35+01:00 7bdf94f
Download a705f1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T06:43:58+01:00 f0af387
Download 15beafa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T05:02:29+01:00 84f15df
Download 59b7006 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 6 2017-11-30T19:16:54+01:00
Download d97d0f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 11 2017-11-30T23:57:41+01:00
Download 715c527 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 6 2017-11-30T13:19:44+01:00
Download 35bd8cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 15 2017-11-30T22:05 CET (sv-comp)
Download 1437fbf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 7 2017-12-02T21:43Z
Download 989a87d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 35 2017-11-30T15:21 CET (sv-comp)

Available Results for the Program from Witness Store SV-COMP '17

Trying to find witnesses for program (2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0, sv-benchmarks/c/bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i, 2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/2a8b53a6466b72e6f5ef202391023c0b4de2efb70382f280d297d4d801c0e4e0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness