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/loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i
programSHA aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9
witnessName results-validated/cpa-seq-validate-violation-witnesses-esbmc-kind.2018-12-08_0449.logfiles/sv-comp19_prop-reachsafety.sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i.files/witness.graphml
witnessSHA 00276f4777b04612da035d919a0d34138a7829b2b13051318aa68f22e9018908

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-08T05:03:41+01:00
inputwitnesshash 73200faba76b02d486b0c21b0bbb7f4e8a1d61e15ee5b1361bad01ac7d0a7c3e
producer CPAchecker 1.7-svn 29852
program-sha256 aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9
programfile ../../sv-benchmarks/c/loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i
programhash aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/00276f4777b04612da035d919a0d34138a7829b2b13051318aa68f22e9018908.graphml
witness-sha256 00276f4777b04612da035d919a0d34138a7829b2b13051318aa68f22e9018908
witness-size 14474
witness-type violation_witness

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

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

Trying to find witnesses for program (aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9, sv-benchmarks/c/loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i, aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9.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 (aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9, sv-benchmarks/c/loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i, aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9.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 (aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9, sv-benchmarks/c/loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i, aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9.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 (aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9, sv-benchmarks/c/loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i, aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9.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 (aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9, sv-benchmarks/c/loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i).

Found 18 witnesses for program sv-benchmarks/c/loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i, aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1694a08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 05:01:57
Download da9715c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 8 2019-12-04T01:19 CET (comp)
Download 248fdfb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness GACAL 18 2019-12-07T23:19 CET (comp)
Download ca78ca9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 14 2019-12-11T21:57:18+01:00 Download 624599f
Download bdce0c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 14 2019-12-11T21:49:39+01:00 Download a1c8cd9
Download 3ab146b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 14 2019-12-11T21:09:03+01:00 Download 1694a08
Download 5843f22 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 14 2019-12-11T20:55:23+01:00 Download 9c87968
Download b491aa7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 75 2019-12-11T20:44:38+01:00 Download 0af228e
Download 82701a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 14 2019-12-08T01:51:41+01:00 Download d2f8961
Download 3502320 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 14 2019-12-08T00:26:13+01:00 Download bde6092
Download 441e702 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 14 2019-12-07T21:15:53+01:00 Download 1106196
Download ee4b5be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 11 2019-12-04T02:58:21+01:00 Download da9715c
Download 0cb2504 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 14 2019-12-03T08:17:53+01:00 Download 445313d
Download 445313d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 14 2019-11-29T14:24:27+01:00
Download d2f8961 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 14 2019-12-07T20:16:48+01:00
Download a1c8cd9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 14 2019-12-01T00:44:45+01:00
Download f755138 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-05T20:21:26+01:00 Download 56efe6e
Download dd81c09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-05T19:34:26+01:00 Download 0b5e458

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

Trying to find witnesses for program (aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9, sv-benchmarks/c/loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i).

Found 21 witnesses for program sv-benchmarks/c/loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i, aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 404c467 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T15:16 CET (sv-comp)
Download 82324a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 5 2018-12-08T01:53:09
Download e0f9c7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 13 2018-12-10T18:53:32+01:00
Download cbb2d69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 14 2018-12-07T18:19:40+01:00
Download 9ffedb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-10T20:38:26+01:00 Download e0f9c7d
Download 4e98e30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-09T20:16:50+01:00 Download 8589238
Download 9160b04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-09T18:21:51+01:00 Download 2f89374
Download 4e92313 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-08T23:43:30+01:00 Download 404c467
Download bfe579b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 11 2018-12-08T22:10:10+01:00 Download 82324a6
Download eb0dbf0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-08T08:06:51+01:00 Download cbb2d69
Download 00276f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-08T05:03:41+01:00 Download 73200fa
Download 3a80cbf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-07T18:46:59+01:00 Download ac2c73e
Download 78c720b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-06T10:19:20+01:00 Download 57cff39
Download 004cf15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-06T09:48:56+01:00 Download 84190b3
Download 95858c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 16 2018-12-06T09:19:23+01:00 Download 71e4856
Download 84190b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 14 2018-12-06T04:51:09+01:00
Download fe124e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-09T21:23:38+01:00 Download a7a04b7
Download e2816e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:53:12+01:00 Download 72fce24
Download af39e4d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:38:28+01:00 Download 086b80f
Download 9dad4ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:41:04+01:00 Download dadca07
Download 9545106 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:11:00+01:00 Download a3e89ad

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

Trying to find witnesses for program (aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9, sv-benchmarks/c/loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i).

Found 18 witnesses for program sv-benchmarks/c/loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i, aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8ebd0df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 4 2017-12-01T22:10 CET (sv-comp)
Download 795c43e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VIAP 768 2017-12-03T04:05 CET (sv-comp)
Download 0407bd1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 9 2017-12-02T17:40Z
Download 0f2c56f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T17:14 CET (sv-comp)
Download 3ae78e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 2 2017-12-01T20:43 CET (sv-comp)
Download d03b7e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 9 2017-12-02T14:58Z
Download 18f560b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T17:41:02.481330
Download ebbf170 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T15:17:57.164160
Download 70f3606 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 6 2017-12-01T21:14 CET (sv-comp)
Download 4c39227 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 6 2017-11-30T23:37 CET (sv-comp)
Download e66f083 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 13 2017-12-02T18:28:24+01:00
Download b430a66 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 13 2017-11-30T15:46:28+01:00
Download d55254b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 18 2017-11-30T11:42:01+01:00
Download 5cfc441 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 11 2017-11-30T11:36:16+01:00
Download 0ec7261 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 13 2017-12-02T03:47:41+01:00
Download df1d9ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 10 2017-11-30T17:49 CET (sv-comp)
Download f2cefc4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 9 2017-12-02T08:59Z
Download ff99f20 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 8 2017-11-30T21:23 CET (sv-comp)

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

Trying to find witnesses for program (aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9, sv-benchmarks/c/loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i, aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/aa3e3a088d745baf78125ccd5627a9c2350b21a28a440a5222651503a55ad4f9.json

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