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/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c
programSHA 9b611c7189054dba1cfb9cb671bdc7a0cc8b4d253b92e25d73767662d842ff10
witnessName results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c.files/witness.graphml
witnessSHA cc872fe1e30032d33c0956dbd70a40a36b7f399ca1ce84a6ef3e5f30df96ff9f

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/cc872fe1e30032d33c0956dbd70a40a36b7f399ca1ce84a6ef3e5f30df96ff9f.json

Key Value
architecture 32bit
creationtime 2017-11-30T23:12 CET (sv-comp)
producer 2LS
program-sha256 9b611c7189054dba1cfb9cb671bdc7a0cc8b4d253b92e25d73767662d842ff10
programfile ../../sv-benchmarks/c/bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c
programhash 322ed2c56e8098dfd507adf1d5eb6a7e1e6354cb
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/cc872fe1e30032d33c0956dbd70a40a36b7f399ca1ce84a6ef3e5f30df96ff9f.graphml
witness-sha256 cc872fe1e30032d33c0956dbd70a40a36b7f399ca1ce84a6ef3e5f30df96ff9f
witness-size 1112566
witness-type correctness_witness

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

Trying to find witnesses for program (9b611c7189054dba1cfb9cb671bdc7a0cc8b4d253b92e25d73767662d842ff10, sv-benchmarks/c/bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c).

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

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

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

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

Found 15 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c, 9b611c7189054dba1cfb9cb671bdc7a0cc8b4d253b92e25d73767662d842ff10
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/9b611c7189054dba1cfb9cb671bdc7a0cc8b4d253b92e25d73767662d842ff10.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 263c082 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 6 2019-12-01 23:14:35
Download 611a234 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 14 2019-12-04T00:50 CET (comp)
Download d8ab8bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 16 2019-12-11T21:59:46+01:00 Download 2b075ff
Download 24ab607 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 16 2019-12-11T21:57:32+01:00 Download 7a42118
Download f3a0ffe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 39 2019-12-11T21:09:23+01:00 Download 263c082
Download 77f3a3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 16 2019-12-08T00:27:21+01:00 Download 7fdd397
Download 07ea892 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 16 2019-12-07T21:17:44+01:00 Download 99da4cc
Download 650d6b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 17 2019-12-04T02:58:26+01:00 Download 611a234
Download 229e52b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 16 2019-12-03T08:10:01+01:00 Download 707378a
Download 707378a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 16 2019-11-30T01:59:46+01:00
Download 7a42118 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 16 2019-12-01T11:57:30+01:00
Download d150b1a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 48 2019-12-11T20:54:59+01:00 Download e04f576
Download 783743d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 48 2019-12-06T02:38:09+01:00 Download 722f96c
Download 47bffc4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 48 2019-12-05T20:21:04+01:00 Download 4d6a18f
Download d789f60 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 48 2019-12-05T19:34:19+01:00 Download bcb4c0c

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

Trying to find witnesses for program (9b611c7189054dba1cfb9cb671bdc7a0cc8b4d253b92e25d73767662d842ff10, sv-benchmarks/c/bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c).

Found 15 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c, 9b611c7189054dba1cfb9cb671bdc7a0cc8b4d253b92e25d73767662d842ff10
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/9b611c7189054dba1cfb9cb671bdc7a0cc8b4d253b92e25d73767662d842ff10.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 37e3d8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T14:00 CET (sv-comp)
Download 1d8e5ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T07:51:40
Download 7e5aa10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 48 2018-12-06T18:44:32+01:00
Download 141a18b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-10T20:05:44+01:00 Download 770fcb7
Download b2eba1a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-09T20:25:43+01:00 Download b461719
Download 0378cf8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-09T17:29:13+01:00 Download ed96360
Download dc18c50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-08T23:10:28+01:00 Download 37e3d8b
Download 23d87a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-08T21:32:32+01:00 Download 1d8e5ba
Download 8cc6f08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-08T05:50:27+01:00 Download 7e5aa10
Download 0c3bc8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-08T02:36:00+01:00 Download 269ebfe
Download 1dc3b53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-06T09:28:30+01:00 Download 8902819
Download 8805ae2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-06T08:57:15+01:00 Download 47055b0
Download 1bb1b21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-06T08:18:08+01:00 Download d0824e7
Download 9fa63db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-06T08:07:10+01:00 Download f250d1e
Download 47055b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 48 2018-12-05T09:37:55+01:00

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

Trying to find witnesses for program (9b611c7189054dba1cfb9cb671bdc7a0cc8b4d253b92e25d73767662d842ff10, sv-benchmarks/c/bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c).

Found 25 witnesses for program sv-benchmarks/c/bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c, 9b611c7189054dba1cfb9cb671bdc7a0cc8b4d253b92e25d73767662d842ff10
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/9b611c7189054dba1cfb9cb671bdc7a0cc8b4d253b92e25d73767662d842ff10.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f9b7c30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 56 2017-12-01T19:11:14+01:00
Download 4700656 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 99 2017-12-03T04:38Z
Download 5f04e16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T00:41 CET (sv-comp)
Download 7912cdc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T12:03:48.617948
Download 3edd47b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T11:58:26.029625
Download e15b8ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 53 2017-12-02T19:34:17+01:00
Download 3450872 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T07:02:16+01:00
Download 1341385 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-03T07:02:08+01:00 10fcd28
Download 80cdcc8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-03T04:14:30+01:00 acf3d70
Download 84a63d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-03T00:56:07+01:00 4a93605
Download 2e7b8af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-02T20:50:59+01:00 159fb01
Download 64ac3f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-02T08:50:43+01:00 55a082e
Download bd98b6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-01T22:32:43+01:00 ffdc525
Download a5d2ff9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-01T08:14:06+01:00 0301b2a
Download 91e8852 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-01T07:13:02+01:00 8b000d8
Download 6dea1bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-01T07:05:38+01:00 a823265
Download 5c74c21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-01T06:47:49+01:00 e55a74f
Download 87211f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-01T06:32:36+01:00 7d3f807
Download f744d10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-12-01T05:20:55+01:00 815cb5c
Download 71db288 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 48 2017-11-30T16:17:58+01:00
Download 0adbde1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 50 2017-12-01T03:32:55+01:00
Download 3095d96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 48 2017-11-30T16:37:38+01:00
Download a9eb391 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 835 2017-11-30T14:25 CET (sv-comp)
Download cb2cbb4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 99 2017-12-02T01:53Z
Download cc872fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 1113 2017-11-30T23:12 CET (sv-comp)

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

Trying to find witnesses for program (9b611c7189054dba1cfb9cb671bdc7a0cc8b4d253b92e25d73767662d842ff10, sv-benchmarks/c/bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c).

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

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