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/recHanoi03_false-unreach-call_true-termination.c
programSHA 8e2c21ca6297fe4a71918b18ff12790ca9294604ce5c399f49c9cbd272336ddb
witnessName results-validated/cpa-seq-validate-violation-witnesses-cpa-seq.2018-12-06_0944.logfiles/sv-comp19_prop-reachsafety.recHanoi03_false-unreach-call_true-termination.c.files/witness.graphml
witnessSHA e831a21442c5b19ff769730867759d4dc5a57b8cba9e20867d88a0b53022b875

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T09:49:08+01:00
inputwitnesshash c58f7e82e3d1c8d54f97e3a50d5db6ff50ad407ba678fe34b2334b3b322a3567
producer CPAchecker 1.7-svn 29852
program-sha256 8e2c21ca6297fe4a71918b18ff12790ca9294604ce5c399f49c9cbd272336ddb
programfile ../../sv-benchmarks/c/bitvector-regression/recHanoi03_false-unreach-call_true-termination.c
programhash 8e2c21ca6297fe4a71918b18ff12790ca9294604ce5c399f49c9cbd272336ddb
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/e831a21442c5b19ff769730867759d4dc5a57b8cba9e20867d88a0b53022b875.graphml
witness-sha256 e831a21442c5b19ff769730867759d4dc5a57b8cba9e20867d88a0b53022b875
witness-size 39587
witness-type violation_witness

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

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

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

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

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

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

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

Found 11 witnesses for program sv-benchmarks/c/bitvector-regression/recHanoi03_false-unreach-call_true-termination.c, 8e2c21ca6297fe4a71918b18ff12790ca9294604ce5c399f49c9cbd272336ddb
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/8e2c21ca6297fe4a71918b18ff12790ca9294604ce5c399f49c9cbd272336ddb.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5defe0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 18:39:25
Download 8716050 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 40 2019-12-11T22:00:26+01:00 Download f4ac926
Download 8a4ac28 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 40 2019-12-08T00:26:18+01:00 Download c0237d6
Download 49a1c7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 40 2019-12-07T21:15:27+01:00 Download a28de3a
Download 2b458e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 48 2019-12-05T20:21:11+01:00 Download 46d7e25
Download 90061cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 40 2019-12-03T08:09:42+01:00 Download 7eedf44
Download 7eedf44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 40 2019-11-30T12:09:59+01:00
Download f4ac926 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 40 2019-12-01T18:46:23+01:00
Download c69526c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:54:28+01:00 Download 0bd0a1e
Download 9ec698c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T01:51:34+01:00 Download 78e6d47
Download 75aef9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 179 2019-12-03T08:58:20+01:00 Download 12f9eac

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

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

Found 15 witnesses for program sv-benchmarks/c/bitvector-regression/recHanoi03_false-unreach-call_true-termination.c, 8e2c21ca6297fe4a71918b18ff12790ca9294604ce5c399f49c9cbd272336ddb
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/8e2c21ca6297fe4a71918b18ff12790ca9294604ce5c399f49c9cbd272336ddb.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 71d97ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T03:17:31
Download 2fa24ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 21 2018-12-07T10:18 CET (sv-comp)
Download 985b6a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 40 2018-12-07T10:08:47+01:00
Download a823d91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 40 2018-12-09T20:53:06+01:00 Download cc97526
Download 778aa2f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 40 2018-12-09T20:40:09+01:00 Download 770e14e
Download d0a7287 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 40 2018-12-09T20:18:46+01:00 Download 8c63d88
Download dbaf4b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 40 2018-12-09T18:22:52+01:00 Download edcfdd1
Download dd41003 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 40 2018-12-08T08:43:32+01:00 Download 985b6a2
Download dfb01af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 41 2018-12-07T17:46:03+01:00 Download 2fa24ac
Download e831a21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 40 2018-12-06T09:49:08+01:00 Download c58f7e8
Download c7a20b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 42 2018-12-06T09:18:40+01:00 Download e481e87
Download 0251bfc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 41 2018-12-06T09:01:41+01:00 Download 2645e0f
Download c58f7e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 40 2018-12-06T05:05:43+01:00
Download 7048faf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 180 2018-12-08T22:11:10+01:00 Download 71d97ae
Download 275ecaf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 6 2018-12-06T10:17:47+01:00 Download 5ba48f7

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

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

Found 13 witnesses for program sv-benchmarks/c/bitvector-regression/recHanoi03_false-unreach-call_true-termination.c, 8e2c21ca6297fe4a71918b18ff12790ca9294604ce5c399f49c9cbd272336ddb
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/8e2c21ca6297fe4a71918b18ff12790ca9294604ce5c399f49c9cbd272336ddb.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8e19f6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 32 2017-12-03T03:35Z
Download de7c15b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 2 2017-12-01T20:30 CET (sv-comp)
Download e013262 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 32 2017-12-02T19:30Z
Download f38bbb7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T12:28:26.612850
Download 46cf618 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T18:56:25.740979
Download 05a50be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 5 2017-12-01T05:39:36+01:00
Download 70d6e1d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 39 2017-11-30T15:39:07+01:00
Download 3afe2da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 11 2017-11-30T21:29:23+01:00
Download 9446cc7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T13:06:54+01:00
Download 9b1bf39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-02T02:33:15+01:00
Download 50caeee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 26 2017-11-30T11:52 CET (sv-comp)
Download 0d95909 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 32 2017-12-02T21:20Z
Download 76cf254 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 6 2017-12-01T19:27 CET (sv-comp)

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

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

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

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