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

This link does not point to a witness, but below is a list of witnesses for the same program.

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

Trying to find witnesses for program (1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e, sv-benchmarks/c/bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c).

Found 0 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c, 1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e.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 (1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e, sv-benchmarks/c/bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c).

Found 0 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c, 1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e.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 (1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e, sv-benchmarks/c/bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c).

Found 0 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c, 1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e.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 (1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e, sv-benchmarks/c/bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c).

Found 0 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c, 1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e.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 (1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e, sv-benchmarks/c/bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c).

Found 14 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c, 1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f0eead8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 5 2019-12-01 17:58:00
Download af246aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 13 2019-12-03T22:47 CET (comp)
Download fb80278 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 15 2019-12-11T21:59:37+01:00 Download 621e36e
Download f4af902 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 15 2019-12-11T21:42:31+01:00 Download c86eaf6
Download b35de4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 35 2019-12-11T21:09:03+01:00 Download f0eead8
Download 361a656 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 15 2019-12-08T00:27:02+01:00 Download a42502a
Download 61a8bc1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 15 2019-12-07T21:17:49+01:00 Download e1c7897
Download 931a264 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 16 2019-12-04T02:58:20+01:00 Download af246aa
Download 82fd3be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 15 2019-12-03T08:09:10+01:00 Download c430a4b
Download c430a4b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 15 2019-11-30T10:46:33+01:00
Download c86eaf6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 15 2019-11-30T23:02:11+01:00
Download a23b0cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 48 2019-12-11T20:54:48+01:00 Download 13bb9fe
Download 352e4fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 48 2019-12-05T20:20:28+01:00 Download 353298a
Download 851b983 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 48 2019-12-05T19:34:03+01:00 Download 2aca82c

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

Trying to find witnesses for program (1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e, sv-benchmarks/c/bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c).

Found 19 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c, 1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 255fbb6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T11:17 CET (sv-comp)
Download 0b3b1fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 12 2018-12-08T03:25:46
Download 39e1a12 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 107 2018-12-07T02:49 CET (sv-comp)
Download 6595e32 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 105 2018-12-10T19:02:17+01:00
Download c3504a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 89 2018-12-08T02:38:23+01:00
Download e20951f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 120 2018-12-10T20:34:57+01:00 Download 6595e32
Download 5919dee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 100 2018-12-09T20:53:18+01:00 Download 20a60fd
Download 0f779d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 100 2018-12-09T20:38:51+01:00 Download c0aa11b
Download 07c6035 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 100 2018-12-09T18:21:07+01:00 Download f706932
Download 4c2bfd4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 101 2018-12-08T23:44:53+01:00 Download 255fbb6
Download 22bfa30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 100 2018-12-08T22:11:06+01:00 Download 0b3b1fc
Download e126144 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 102 2018-12-08T08:36:27+01:00 Download c3504a2
Download 999af0d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 146 2018-12-08T05:00:48+01:00 Download 5e28165
Download 929723e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 180 2018-12-07T17:45:10+01:00 Download 39e1a12
Download 59a4911 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 121 2018-12-06T10:19:49+01:00 Download 3f631e9
Download e25c55b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 100 2018-12-06T09:48:08+01:00 Download de1f391
Download 9f72082 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 131 2018-12-06T09:18:59+01:00 Download 93a2f45
Download de1f391 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 87 2018-12-05T22:46:52+01:00
Download b1f23f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-06T09:42:10+01:00 Download ad59233

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

Trying to find witnesses for program (1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e, sv-benchmarks/c/bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c).

Found 14 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c, 1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 61c41a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 101 2017-12-03T04:00Z
Download dcf2180 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T13:56 CET (sv-comp)
Download 82afdd8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 12 2017-12-01T22:09:59.659126
Download 7f863d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 12 2017-12-01T20:22:31.611238
Download 69666c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 24 2017-11-30T19:04 CET (sv-comp)
Download e29dacd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 105 2017-12-02T23:39:51+01:00
Download f632aaf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 77 2017-11-30T22:17:43+01:00
Download 005f6e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 100 2017-11-30T23:14:45+01:00
Download c412f39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 47 2017-12-01T22:22:59+01:00
Download b74f448 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 120 2017-11-30T19:16 CET (sv-comp)
Download 917dc25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 101 2017-12-02T20:43Z
Download 438408d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 67 2017-11-30T15:29 CET (sv-comp)
Download f56e4c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 27 2017-12-01T21:26 CET (sv-comp)
Download ebcdccc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-01T22:37:16+01:00 526e125

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

Trying to find witnesses for program (1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e, sv-benchmarks/c/bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c).

Found 0 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c, 1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/1f2ef3327eef810869ffdab8b668133a62c90b2c872ff7c04665020b83e7207e.json

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