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-regression/integerpromotion_false-unreach-call_true-termination.c
programSHA a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70
witnessName results-validated/cpa-seq-validate-violation-witnesses-uautomizer.2018-12-09_2030.logfiles/sv-comp19_prop-reachsafety.integerpromotion_false-unreach-call_true-termination.c.files/witness.graphml
witnessSHA 0dc3abcb97d0398452fb75834b7017408fababc83e5933a3cdd5cdd132cc676c

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-09T20:39:57+01:00
inputwitnesshash a3a067d06d8a565688f59048ce86b8f354adabf219bfba3bbdeeddc749189458
producer CPAchecker 1.7-svn 29852
program-sha256 a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70
programfile ../../sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c
programhash a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/0dc3abcb97d0398452fb75834b7017408fababc83e5933a3cdd5cdd132cc676c.graphml
witness-sha256 0dc3abcb97d0398452fb75834b7017408fababc83e5933a3cdd5cdd132cc676c
witness-size 4513
witness-type violation_witness

This witness was created for this program (cf. table above, a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70).

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

Trying to find witnesses for program (a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70, sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c, a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70.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 (a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70, sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c, a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70.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 (a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70, sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c, a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70.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 (a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70, sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c, a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70.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 (a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70, sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c).

Found 19 witnesses for program sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c, a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 25868be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 20:02:02
Download 0fb046d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 4 2019-12-04T01:03 CET (comp)
Download 386869a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T21:40:41+01:00 Download 7637deb
Download 8ea7109 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T21:09:05+01:00 Download 25868be
Download 244d1ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:54:29+01:00 Download fa89db0
Download 708bd74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:44:34+01:00 Download fecafa6
Download 72aea48 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 4 2019-12-08T01:52:07+01:00 Download 6073c9c
Download b3c0622 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 4 2019-12-08T00:26:30+01:00 Download 5cbd4ab
Download 8e588b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T21:16:10+01:00 Download edaa94a
Download f3cd0be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 4 2019-12-06T02:41:08+01:00 Download d41767a
Download 41f4a52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T20:20:30+01:00 Download 5446c4a
Download 39e0b87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 4 2019-12-04T02:58:17+01:00 Download 0fb046d
Download a10f99b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 4 2019-12-03T08:56:48+01:00 Download 63d126d
Download ddb5029 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 4 2019-12-03T08:07:50+01:00 Download 96363ac
Download 96363ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 4 2019-11-29T20:35:20+01:00
Download 6073c9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 4 2019-12-07T19:13:35+01:00
Download 7637deb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 4 2019-12-01T16:13:17+01:00
Download 2d6fa82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:34:00+01:00 Download fb9249d
Download e585c25 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:04 CET (comp)

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

Trying to find witnesses for program (a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70, sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c).

Found 27 witnesses for program sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c, a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 95d9b28 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T14:09 CET (sv-comp)
Download 20f33a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T12:38:23
Download 4a178a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 4 2018-12-07T12:22 CET (sv-comp)
Download 2021b34 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 4 2018-12-10T18:15:58+01:00
Download 82f017c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-07T19:22:10+01:00
Download 416781c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-10T20:35:15+01:00 Download 2021b34
Download 7609bf6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-10T10:48:42+01:00 Download c477584
Download 4cea92d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:53:11+01:00 Download a50d296
Download 0dc3abc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:39:57+01:00 Download a3a067d
Download ba9b2ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:28:45+01:00 Download 9366396
Download 1e986ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T18:14:45+01:00 Download e0711be
Download 0247c53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T23:44:41+01:00 Download 95d9b28
Download 3f1bac3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T22:08:55+01:00 Download 20f33a5
Download eab0c6d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T08:25:40+01:00 Download 82f017c
Download 0bff5d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T05:00:00+01:00 Download 7e673b7
Download 4647f35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T03:41:16+01:00 Download c477584
Download 1545040 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T18:47:02+01:00 Download 4c6fe01
Download f1d09f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T17:45:45+01:00 Download 4a178a7
Download f6e703b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T01:10:10+01:00 Download 802258f
Download a1098ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T10:17:40+01:00 Download 11cd7f2
Download 3a9ba5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:48:56+01:00 Download 9786b54
Download 1b5ffbd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:18:30+01:00 Download 944f0e0
Download f7ebc7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:06:55+01:00 Download 0517650
Download 9786b54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-05T13:22:21+01:00
Download 7c6dd49 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:42:17+01:00 Download c809107
Download 6d0ba0d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T09:22 CET (sv-comp)
Download aa0f82c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T10:49 CET (sv-comp)

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

Trying to find witnesses for program (a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70, sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c).

Found 21 witnesses for program sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c, a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download bb6d7c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T22:48 CET (sv-comp)
Download 357b73d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 4 2017-12-03T03:30Z
Download 053f855 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T15:18 CET (sv-comp)
Download 1f6b63d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 3 2017-12-01T21:07 CET (sv-comp)
Download e1f9b22 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 4 2017-12-02T13:00Z
Download 4b0d9f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T05:18:06.539530
Download 1e98607 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T10:49:20.316282
Download e6fb6fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-12-01T17:11 CET (sv-comp)
Download 9e36576 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-11-30T20:53 CET (sv-comp)
Download 675a924 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 4 2017-12-02T23:30:44+01:00
Download 60a3f18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T02:25:29+01:00
Download 413c44f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 6 2017-11-30T17:17:00+01:00
Download f355732 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 4 2017-11-30T19:57:36+01:00
Download 4a03d10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 4 2017-12-01T23:01:11+01:00
Download b9d4892 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 4 2017-11-30T18:30 CET (sv-comp)
Download 40255b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 4 2017-12-02T07:20Z
Download c809107 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 4 2017-11-30T14:25 CET (sv-comp)
Download ac22437 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T01:37:35.579420
Download b6d0dfa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T14:23:14.919546
Download 550c7ed Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 4 2017-12-01T14:51 CET (sv-comp)
Download f3ebe18 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 7 2017-12-01T12:54 CET (sv-comp)

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

Trying to find witnesses for program (a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70, sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/bitvector-regression/integerpromotion_false-unreach-call_true-termination.c, a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/a966fe3c643e09c8fc5207ca6c3eead2c84d01c2a7e856a045413ee9b39cec70.json

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