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/ldv-regression/alt_test_true-termination.c_false-unreach-call.i
programSHA 9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523
witnessName results-validated/cpa-seq-validate-violation-witnesses-divine-explicit.2018-12-10_1048.logfiles/sv-comp19_prop-reachsafety.alt_test_true-termination.c_false-unreach-call.i.files/witness.graphml
witnessSHA de5c1b57faf17976f5fc43fbb238afe67dedd817c5459d8986c42bdfce6930ab

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-10T10:49:00+01:00
inputwitnesshash 9f35a144471602579dddd55f06328844d819034a70e97cd323df2894d5f1e356
producer CPAchecker 1.7-svn 29852
program-sha256 9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523
programfile ../../sv-benchmarks/c/ldv-regression/alt_test_true-termination.c_false-unreach-call.i
programhash 9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/de5c1b57faf17976f5fc43fbb238afe67dedd817c5459d8986c42bdfce6930ab.graphml
witness-sha256 de5c1b57faf17976f5fc43fbb238afe67dedd817c5459d8986c42bdfce6930ab
witness-size 8662
witness-type violation_witness

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

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

Trying to find witnesses for program (9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523, sv-benchmarks/c/ldv-regression/alt_test_true-termination.c_false-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/alt_test_true-termination.c_false-unreach-call.i, 9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523.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 (9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523, sv-benchmarks/c/ldv-regression/alt_test_true-termination.c_false-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/alt_test_true-termination.c_false-unreach-call.i, 9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523.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 (9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523, sv-benchmarks/c/ldv-regression/alt_test_true-termination.c_false-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/alt_test_true-termination.c_false-unreach-call.i, 9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523.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 (9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523, sv-benchmarks/c/ldv-regression/alt_test_true-termination.c_false-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/alt_test_true-termination.c_false-unreach-call.i, 9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523.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 (9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523, sv-benchmarks/c/ldv-regression/alt_test_true-termination.c_false-unreach-call.i).

Found 18 witnesses for program sv-benchmarks/c/ldv-regression/alt_test_true-termination.c_false-unreach-call.i, 9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fc46a79 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 01:59:53
Download 5b6a706 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T21:58:01+01:00 Download b7703bf
Download 47c7141 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T21:42:34+01:00 Download 85418f1
Download 15a1623 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T21:09:47+01:00 Download fc46a79
Download 5bd6afc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T20:54:51+01:00 Download 7b054a6
Download 5a2a99c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T20:44:42+01:00 Download 03e956c
Download 54c39ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-08T01:51:16+01:00 Download 91c37b3
Download 33adbbe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-08T00:27:24+01:00 Download 977401a
Download 0afdc61 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-08T00:06:23+01:00 Download a773a64
Download 67677da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-07T21:14:27+01:00 Download 3af2eba
Download 550fbca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-06T02:39:41+01:00 Download f18da3c
Download b704b9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-05T20:21:29+01:00 Download b83f503
Download 6daeac8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-05T19:34:14+01:00 Download 0b2adaf
Download c39fcaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-03T08:57:16+01:00 Download f6aa480
Download 85300b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 9 2019-12-03T08:17:37+01:00 Download d4d5ce4
Download d4d5ce4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 8 2019-11-30T06:16:36+01:00
Download 91c37b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 8 2019-12-07T16:21:10+01:00
Download b7703bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 9 2019-12-01T01:35:15+01:00

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

Trying to find witnesses for program (9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523, sv-benchmarks/c/ldv-regression/alt_test_true-termination.c_false-unreach-call.i).

Found 28 witnesses for program sv-benchmarks/c/ldv-regression/alt_test_true-termination.c_false-unreach-call.i, 9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 49c5fde Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T12:04 CET (sv-comp)
Download f480e18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T07:52:56
Download 29109f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 6 2018-12-07T13:10 CET (sv-comp)
Download 0b74a2e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 8 2018-12-10T19:05:47+01:00
Download c9f1abf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 9 2018-12-08T02:55:48+01:00
Download 4fad9c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-10T20:34:49+01:00 Download 0b74a2e
Download de5c1b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-10T10:49:00+01:00 Download 9f35a14
Download ab8e357 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-09T20:53:10+01:00 Download 6a6d748
Download a0aeaf8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-09T20:38:47+01:00 Download c9a608a
Download 717d86a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-09T20:32:23+01:00 Download 0b8f679
Download 062e7c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-09T18:09:59+01:00 Download 7aed18f
Download 9f7585c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-08T23:43:58+01:00 Download 49c5fde
Download d3dd672 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-08T22:08:59+01:00 Download f480e18
Download 51559a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-08T08:35:19+01:00 Download c9f1abf
Download 8927e12 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-08T04:52:00+01:00 Download 82a7788
Download 885eeb7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-08T04:30:38+01:00 Download 9f35a14
Download 1feb12a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-07T18:48:29+01:00 Download 62e70d3
Download a397e48 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-07T17:45:33+01:00 Download 29109f6
Download ccb866f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-07T09:28:37+01:00 Download c013d03
Download b7a35e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-07T01:10:23+01:00 Download e87a79a
Download 7eaad6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-06T10:17:52+01:00 Download 8216414
Download 9b7a54c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:48:12+01:00 Download 8f16a12
Download ac56954 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:41:28+01:00 Download a4b6ea9
Download d2c6828 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:14:57+01:00 Download e1e25dc
Download 4f7826d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:12:00+01:00 Download ddba469
Download 8f16a12 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-06T06:48:34+01:00
Download 9137828 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T11:45 CET (sv-comp)
Download e3b3136 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-06T23:10 CET (sv-comp)

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

Trying to find witnesses for program (9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523, sv-benchmarks/c/ldv-regression/alt_test_true-termination.c_false-unreach-call.i).

Found 22 witnesses for program sv-benchmarks/c/ldv-regression/alt_test_true-termination.c_false-unreach-call.i, 9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 851ba1f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T23:45 CET (sv-comp)
Download 712f7d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 8 2017-12-03T03:57Z
Download a45a4c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T06:53 CET (sv-comp)
Download c013d03 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness PredatorHP 4 2017-12-01T20:38 CET (sv-comp)
Download 8aa5c0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 4 2017-12-01T20:32 CET (sv-comp)
Download dfc91ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 8 2017-12-02T12:37Z
Download 7545d4c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Forester 5 2017-12-01T18:15 CET (sv-comp)
Download 970043c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T00:43:54.006095
Download 23d03d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T16:59:31.583389
Download efc147a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-12-01T18:13 CET (sv-comp)
Download 85d8c0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-11-30T16:15 CET (sv-comp)
Download 87cfdad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 9 2017-11-30T14:03:24+01:00
Download 63a4d81 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 12 2017-11-30T11:50:12+01:00
Download ee4614f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 7 2017-12-01T03:39:28+01:00
Download 69ef2e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 8 2017-12-02T05:40:41+01:00
Download 7debf07 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 6 2017-12-01T00:30 CET (sv-comp)
Download bc724eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 8 2017-12-02T09:57Z
Download bb07601 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 6 2017-11-30T22:57 CET (sv-comp)
Download 4992c38 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T21:54:34.986560
Download c192da3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T12:14:35.942691
Download 8bdcbda Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 8 2017-12-01T15:46 CET (sv-comp)
Download 80c3e3c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 29 2017-12-01T12:25 CET (sv-comp)

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

Trying to find witnesses for program (9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523, sv-benchmarks/c/ldv-regression/alt_test_true-termination.c_false-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/alt_test_true-termination.c_false-unreach-call.i, 9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/9c3f4e46fc943dd3c94a1ec354532ab5e8570246d18af0d828d96532c7444523.json

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