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/recursive-simple/id_i25_o25_true-unreach-call_true-termination.c
programSHA 04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a
witnessName results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.id_i25_o25_true-unreach-call_true-termination.c.files/witness.graphml
witnessSHA d2d918d20d346f6ef1aad7aff8ceea91e329bf6bd2e4a6235142e48709e528be

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-11-30T14:41:25+01:00
producer CPAchecker 1.6.1-svn 26725
program-sha256 04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a
programfile ../../sv-benchmarks/c/recursive-simple/id_i25_o25_true-unreach-call_true-termination.c
programhash 980109aaf5797fcdc56688cd1127831babfd66a2
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/d2d918d20d346f6ef1aad7aff8ceea91e329bf6bd2e4a6235142e48709e528be.graphml
witness-sha256 d2d918d20d346f6ef1aad7aff8ceea91e329bf6bd2e4a6235142e48709e528be
witness-size 4574
witness-type violation_witness

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

Trying to find witnesses for program (04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a, sv-benchmarks/c/recursive-simple/id_i25_o25_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_i25_o25_true-unreach-call_true-termination.c, 04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a.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 (04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a, sv-benchmarks/c/recursive-simple/id_i25_o25_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_i25_o25_true-unreach-call_true-termination.c, 04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a.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 (04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a, sv-benchmarks/c/recursive-simple/id_i25_o25_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_i25_o25_true-unreach-call_true-termination.c, 04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a.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 (04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a, sv-benchmarks/c/recursive-simple/id_i25_o25_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_i25_o25_true-unreach-call_true-termination.c, 04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a.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 (04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a, sv-benchmarks/c/recursive-simple/id_i25_o25_true-unreach-call_true-termination.c).

Found 16 witnesses for program sv-benchmarks/c/recursive-simple/id_i25_o25_true-unreach-call_true-termination.c, 04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b024a8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T23:42 CET (comp)
Download f24459a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:22:26+01:00 Download 5606226
Download 716000c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:16:15+01:00 Download 7043fe1
Download 7867418 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:14:04+01:00 Download bff3d07
Download 0f8c912 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:02:16+01:00 Download 38118af
Download 124ca9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T00:36:32+01:00 Download 193e821
Download 3a9332a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T23:36:32+01:00 Download 895504f
Download 70e8ed1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T19:45:20+01:00 Download 793e36a
Download 3a6f0c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-06T02:04:27+01:00 Download 0b83c01
Download 13e8338 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-05T19:12:59+01:00 Download 2bcba90
Download 533112c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-04T02:07:30+01:00 Download b024a8e
Download d659e7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-11-30T19:52:25+01:00 Download 22f3882
Download 1610944 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-11-30T17:19:12+01:00 Download a1f58af
Download a1f58af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 5 2019-11-30T03:19:57+01:00
Download 7043fe1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 5 2019-12-01T19:03:39+01:00
Download 105eb48 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:27 CET (comp)

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

Trying to find witnesses for program (04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a, sv-benchmarks/c/recursive-simple/id_i25_o25_true-unreach-call_true-termination.c).

Found 22 witnesses for program sv-benchmarks/c/recursive-simple/id_i25_o25_true-unreach-call_true-termination.c, 04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fcc590b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T04:56 CET (sv-comp)
Download f01d6ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T01:06:18
Download fd82dea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T09:26 CET (sv-comp)
Download fb210ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-06T21:17:57+01:00
Download 18e71cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T10:31:22+01:00 Download 6eca2bc
Download d889e2e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T21:06:32+01:00 Download 75fb3d2
Download ec2633f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:30:15+01:00 Download 35c43be
Download 31613b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T19:39:48+01:00 Download 6283ca3
Download a2dc1c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T17:38:23+01:00 Download 2c2ccde
Download c471606 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T23:08:17+01:00 Download fcc590b
Download 72af54d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T21:33:27+01:00 Download f01d6ac
Download 428bd46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T07:13:54+01:00 Download fb210ce
Download a348ec4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T03:34:09+01:00 Download c4726b5
Download 309e79f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T02:11:55+01:00 Download 6eca2bc
Download be6e748 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T17:44:31+01:00 Download 69a7c0e
Download b8130ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T16:38:15+01:00 Download fd82dea
Download bbd58d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:28:46+01:00 Download c380637
Download 18cb64e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:01:24+01:00 Download de730b1
Download 1ae63b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T08:29:28+01:00 Download 7dd9ccf
Download de730b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-05T11:56:17+01:00
Download d0b1946 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T12:16 CET (sv-comp)
Download b21f77a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T00:58 CET (sv-comp)

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

Trying to find witnesses for program (04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a, sv-benchmarks/c/recursive-simple/id_i25_o25_true-unreach-call_true-termination.c).

Found 31 witnesses for program sv-benchmarks/c/recursive-simple/id_i25_o25_true-unreach-call_true-termination.c, 04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c5e53a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 9 2017-12-01T00:21:46+01:00
Download d2d918d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T14:41:25+01:00
Download 3ccf756 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-01T22:08:43+01:00
Download 69a7c0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T23:20 CET (sv-comp)
Download 15551da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness VIAP 24 2017-12-03T03:51 CET (sv-comp)
Download 5092bbc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 6 2017-12-03T05:19Z
Download d4dd09f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T05:55 CET (sv-comp)
Download 11ce032 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 3 2017-12-01T20:25 CET (sv-comp)
Download 8995e2a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 6 2017-12-02T10:26Z
Download 568c64c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T22:13:43.479361
Download 1f28dbc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T10:42:01.095078
Download abb5acc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T12:04:40.726695
Download 7f253b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T09:45:50.369074
Download 5b0a749 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 4 2017-12-01T15:37 CET (sv-comp)
Download 2130c7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 6 2017-12-01T00:10:23+01:00
Download 6fbbe97 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T06:50:45+01:00 e53959b
Download 92c0605 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T04:22:16+01:00 b9ac80b
Download 552cc0d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T00:49:42+01:00 d6b0029
Download da2eb17 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T23:59:08+01:00 fe793a6
Download d42e7db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T20:26:37+01:00 95968c7
Download 2ed43ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T08:18:04+01:00 28c375b
Download aed06b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T00:16:14+01:00 e33a27a
Download d668fcd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T22:21:02+01:00 0b6724b
Download 86a71b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T22:08:42+01:00 0b6c037
Download 50d1428 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T08:13:35+01:00 3658974
Download 08ede38 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T05:27:25+01:00 f0acb5d
Download 621a212 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T05:26:29+01:00 3b8a447
Download f559619 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-11-30T21:15:48+01:00
Download f35de7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 19 2017-11-30T11:49 CET (sv-comp)
Download 502f3f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 6 2017-12-02T00:18Z
Download 7443e6c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 19 2017-12-01T17:46 CET (sv-comp)

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

Trying to find witnesses for program (04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a, sv-benchmarks/c/recursive-simple/id_i25_o25_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/id_i25_o25_true-unreach-call_true-termination.c, 04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/04b7e487ebc8a7016152729844580890b18e381e315393f645671d9eb80e031a.json

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