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/float-benchs/Rump_double_true-unreach-call_true-termination.c
programSHA a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8
witnessName results-validated/cpa-seq-validate-correctness-witnesses-pinaka.2018-12-07_1617.logfiles/sv-comp19_prop-reachsafety.Rump_double_true-unreach-call_true-termination.c.files/witness.graphml
witnessSHA c488ad39c13e91b9fc8996b62ce55344782a837049f24ec12896a3900de96088

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-07T16:28:46+01:00
inputwitnesshash 0f1df23daec40a0d20950175fb5718aa99aa9a87fac8b70bb33e519cb636b89e
producer CPAchecker 1.7-svn 29852
program-sha256 a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8
programfile ../../sv-benchmarks/c/float-benchs/Rump_double_true-unreach-call_true-termination.c
programhash a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/c488ad39c13e91b9fc8996b62ce55344782a837049f24ec12896a3900de96088.graphml
witness-sha256 c488ad39c13e91b9fc8996b62ce55344782a837049f24ec12896a3900de96088
witness-size 4183
witness-type correctness_witness

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

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

Trying to find witnesses for program (a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8, sv-benchmarks/c/float-benchs/Rump_double_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/Rump_double_true-unreach-call_true-termination.c, a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8.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 (a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8, sv-benchmarks/c/float-benchs/Rump_double_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/Rump_double_true-unreach-call_true-termination.c, a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8.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 (a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8, sv-benchmarks/c/float-benchs/Rump_double_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/Rump_double_true-unreach-call_true-termination.c, a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8.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 (a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8, sv-benchmarks/c/float-benchs/Rump_double_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/Rump_double_true-unreach-call_true-termination.c, a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8.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 (a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8, sv-benchmarks/c/float-benchs/Rump_double_true-unreach-call_true-termination.c).

Found 17 witnesses for program sv-benchmarks/c/float-benchs/Rump_double_true-unreach-call_true-termination.c, a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3e5ed90 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T23:16 CET (comp)
Download 23910bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:23:07+01:00 Download 1165d9e
Download 15ab8ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:08:52+01:00 Download 324a131
Download 79da527 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:03:12+01:00 Download 7ad250e
Download 7800219 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-08T00:36:17+01:00 Download 384c70f
Download c6a5b20 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:47:29+01:00 Download 6acb1eb
Download ca4caec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:20:59+01:00 Download 7c02d1f
Download 4717b35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T19:46:13+01:00 Download 0f4e822
Download 2bc439d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:13:10+01:00 Download 4d6111a
Download 3525e8a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:03:01+01:00 Download b8ee046
Download 4f3683d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-04T02:07:42+01:00 Download 3e5ed90
Download 9e33f86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-11-30T19:05:49+01:00 Download c30fb16
Download bf6858b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-11-30T16:42:56+01:00 Download 721a1f4
Download 721a1f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 4 2019-11-30T13:20:32+01:00
Download 384c70f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 4 2019-12-07T20:45:55+01:00
Download 324a131 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 4 2019-12-01T01:50:31+01:00
Download 6acb1eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness BRICK 3 2019-12-07T21:40:24Z

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

Trying to find witnesses for program (a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8, sv-benchmarks/c/float-benchs/Rump_double_true-unreach-call_true-termination.c).

Found 20 witnesses for program sv-benchmarks/c/float-benchs/Rump_double_true-unreach-call_true-termination.c, a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download cd7bd98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T16:32 CET (sv-comp)
Download 75094ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T05:24:34
Download 0f1df23 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T14:33 CET (sv-comp)
Download ea8e25e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-07T09:12:13+01:00
Download 524bd42 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-10T20:16:36+01:00 Download f8ef6d2
Download ba2567c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-10T10:31:30+01:00 Download 22b8b52
Download 6cb4f7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:26:11+01:00 Download 5429e01
Download 00c29bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T17:27:47+01:00 Download c08d9d7
Download 7a78eac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T23:16:16+01:00 Download cd7bd98
Download e49013d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T21:15:07+01:00 Download 75094ce
Download 1ecd35f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T06:22:51+01:00 Download ea8e25e
Download 461626e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T03:36:18+01:00 Download 2a29348
Download 79741cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T02:41:57+01:00 Download 22b8b52
Download ee1d6af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T17:44:55+01:00 Download 7603918
Download c488ad3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T16:28:46+01:00 Download 0f1df23
Download 2c720d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:28:18+01:00 Download 25bd157
Download 38dbd53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:53:23+01:00 Download 052d8ba
Download 454bc58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:14:48+01:00 Download 4a47832
Download 9b3f460 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T07:22:52+01:00 Download 9899349
Download 052d8ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T01:01:55+01:00

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

Trying to find witnesses for program (a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8, sv-benchmarks/c/float-benchs/Rump_double_true-unreach-call_true-termination.c).

Found 27 witnesses for program sv-benchmarks/c/float-benchs/Rump_double_true-unreach-call_true-termination.c, a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 81c1f66 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 5 2017-12-01T20:36:28+01:00
Download 7603918 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:38 CET (sv-comp)
Download cd0e362 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 5 2017-12-03T04:10Z
Download 2349f84 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T13:53 CET (sv-comp)
Download 7831c63 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T22:22:16.028005
Download 84fccc8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T09:11:31.919274
Download ebf1896 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-03T02:11:24+01:00
Download 5e41a25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-11-30T16:20:02+01:00
Download 4515eeb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T07:01:43+01:00 5dabbc9
Download faadbd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T04:08:42+01:00 774ed4a
Download 967a260 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T02:28:26+01:00 2635d77
Download 7529644 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T20:03:19+01:00 80cb64c
Download b00038a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T07:41:19+01:00 9ef86c7
Download 5c725e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T00:15:47+01:00 a791fcd
Download 8fa18c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T22:37:41+01:00 3476a78
Download 0d4c2fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T08:13:31+01:00 24cfc57
Download 59f4a23 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T07:05:27+01:00 406eb69
Download 8f236d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T06:58:05+01:00 1a9b7f1
Download 4a15f7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T06:33:39+01:00 64f4dff
Download b992a6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T06:28:10+01:00 6e7c307
Download ddc6f82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T06:17:25+01:00 0726c95
Download 1eba9cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T01:42:04+01:00
Download 6b5c1eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 8 2017-11-30T21:51:39+01:00
Download 38d1d40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 4 2017-12-01T03:55:32+01:00
Download 9ee2ca8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 5 2017-11-30T22:49 CET (sv-comp)
Download e44718f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 5 2017-12-02T01:17Z
Download 456c955 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 8 2017-11-30T23:48 CET (sv-comp)

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

Trying to find witnesses for program (a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8, sv-benchmarks/c/float-benchs/Rump_double_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/Rump_double_true-unreach-call_true-termination.c, a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/a69a4c45f3dab569fd6d3ad91588389b8a69f721c890055a9b54715fbf0546e8.json

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