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/test26_false-unreach-call_true-termination.c
programSHA bb493101aba486c02b83eec146067430a253dc574b61bbcd4c41584f28101760
witnessName results-verified/map2check.2018-12-06_1220.logfiles/sv-comp19_prop-reachsafety.test26_false-unreach-call_true-termination.c.files/witness.graphml
witnessSHA bfea717cebc75001199c50b4c64aa743deae4af13f440c8a1f351657e701830f

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-06T13:11 CET (sv-comp)
producer Map2Check
programfile /tmp/vcloud-vcloud-master/worker/working_dir_53ae0988-6a1a-4ccf-94cf-57b09eb864a8/bin-2019/map2check/../../sv-benchmarks/c/ldv-regression/test26_false-unreach-call_true-termination.c
programhash e02278ee7d9986faf1ae0635ee11725f823e79f3
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/bfea717cebc75001199c50b4c64aa743deae4af13f440c8a1f351657e701830f.graphml
witness-sha256 bfea717cebc75001199c50b4c64aa743deae4af13f440c8a1f351657e701830f
witness-size 2331
witness-type violation_witness

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

Trying to find witnesses for program (bb493101aba486c02b83eec146067430a253dc574b61bbcd4c41584f28101760, sv-benchmarks/c/ldv-regression/test26_false-unreach-call_true-termination.c).

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

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

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

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

Found 21 witnesses for program sv-benchmarks/c/ldv-regression/test26_false-unreach-call_true-termination.c, bb493101aba486c02b83eec146067430a253dc574b61bbcd4c41584f28101760
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/bb493101aba486c02b83eec146067430a253dc574b61bbcd4c41584f28101760.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0657f33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-02 05:53:18
Download a6038aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 4 2019-12-04T00:14 CET (comp)
Download b09e322 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T21:59:17+01:00 Download 8d34f91
Download b372944 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T21:41:58+01:00 Download 7ecdce4
Download bd9808c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T21:09:14+01:00 Download 0657f33
Download e64f437 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:54:19+01:00 Download 47a8eba
Download 0684cc7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:44:27+01:00 Download 15652fb
Download 003cfdb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T01:52:33+01:00 Download 41c158e
Download 92d58ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T00:26:54+01:00 Download 6b042e7
Download 227c38b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T00:06:24+01:00 Download 7b07fde
Download ffb023c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T21:14:28+01:00 Download b803c7a
Download 7fee860 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-06T02:40:27+01:00 Download 3a460f9
Download 6810898 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-05T20:20:12+01:00 Download 6d03ec6
Download 9a998be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-04T02:58:01+01:00 Download a6038aa
Download a0f200c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-03T08:57:54+01:00 Download bf9d30d
Download c68f3f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-03T08:10:07+01:00 Download c4ae619
Download c4ae619 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 5 2019-11-29T23:28:00+01:00
Download 41c158e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 5 2019-12-07T16:40:32+01:00
Download 7ecdce4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 5 2019-11-30T23:02:12+01:00
Download e24dc8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:34:31+01:00 Download a453e9c
Download e70ca42 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:19 CET (comp)

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

Trying to find witnesses for program (bb493101aba486c02b83eec146067430a253dc574b61bbcd4c41584f28101760, sv-benchmarks/c/ldv-regression/test26_false-unreach-call_true-termination.c).

Found 27 witnesses for program sv-benchmarks/c/ldv-regression/test26_false-unreach-call_true-termination.c, bb493101aba486c02b83eec146067430a253dc574b61bbcd4c41584f28101760
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/bb493101aba486c02b83eec146067430a253dc574b61bbcd4c41584f28101760.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f2b3ad4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T03:18 CET (sv-comp)
Download 6f51975 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 3 2018-12-08T06:11:05
Download 47af040 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 4 2018-12-07T12:55 CET (sv-comp)
Download 60cfa1b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 5 2018-12-10T18:09:37+01:00
Download 7719c13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-07T07:46:53+01:00
Download 257e8a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-10T20:36:29+01:00 Download 60cfa1b
Download 46c7d44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-10T10:48:41+01:00 Download a394814
Download 45e4347 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:53:07+01:00 Download 5353c5f
Download 8a78727 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:40:10+01:00 Download 9ca18ca
Download a2ad7c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:21:17+01:00 Download b277556
Download 6eaa00b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T18:21:06+01:00 Download 1e1f290
Download c1f60b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T23:43:06+01:00 Download f2b3ad4
Download f4a3d17 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T22:11:21+01:00 Download 6f51975
Download 827351b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T08:23:47+01:00 Download 7719c13
Download 1d72bee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T04:58:28+01:00 Download 17d15b0
Download 32356ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T04:29:54+01:00 Download a394814
Download 4091366 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T17:43:02+01:00 Download 47af040
Download 26d10a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T09:30:24+01:00 Download 30c9e2a
Download aca0e45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T01:18:41+01:00 Download bfea717
Download 3b307ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T10:18:21+01:00 Download 0894fb9
Download 85048c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:48:55+01:00 Download 82faed3
Download 47df7a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:18:05+01:00 Download 9ab25b0
Download 1994fab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:17:52+01:00 Download 5b6ae1d
Download 82faed3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T07:12:21+01:00
Download ab740cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:42:08+01:00 Download bef9886
Download 0cfe747 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T03:06 CET (sv-comp)
Download ae0d945 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T14:38 CET (sv-comp)

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

Trying to find witnesses for program (bb493101aba486c02b83eec146067430a253dc574b61bbcd4c41584f28101760, sv-benchmarks/c/ldv-regression/test26_false-unreach-call_true-termination.c).

Found 22 witnesses for program sv-benchmarks/c/ldv-regression/test26_false-unreach-call_true-termination.c, bb493101aba486c02b83eec146067430a253dc574b61bbcd4c41584f28101760
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/bb493101aba486c02b83eec146067430a253dc574b61bbcd4c41584f28101760.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5186582 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 5 2017-12-03T03:21Z
Download 2b4de00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T14:07 CET (sv-comp)
Download 30c9e2a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness PredatorHP 4 2017-12-01T20:46 CET (sv-comp)
Download fc6c518 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 3 2017-12-01T21:39 CET (sv-comp)
Download b2147ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 5 2017-12-02T20:06Z
Download b6fd1ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Forester 5 2017-12-01T17:55 CET (sv-comp)
Download e9192ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T03:48:00.912805
Download d371678 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T15:19:46.010567
Download 4ed133e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-12-01T17:18 CET (sv-comp)
Download 833a7a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-12-01T02:29 CET (sv-comp)
Download fa4a7de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 5 2017-12-02T21:44:08+01:00
Download 3a9db59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 4 2017-11-30T15:07:39+01:00
Download f3a5c89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 7 2017-12-01T00:46:21+01:00
Download 9f4c33a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 4 2017-12-01T00:51:44+01:00
Download ae08dae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 5 2017-12-01T20:23:29+01:00
Download a3a28b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 4 2017-11-30T13:47 CET (sv-comp)
Download 439dd80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 5 2017-12-02T09:46Z
Download bef9886 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 3 2017-11-30T23:07 CET (sv-comp)
Download 5b56eb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T01:40:42.741486
Download 1cf390b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T12:47:25.045225
Download be57b10 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 4 2017-12-01T14:20 CET (sv-comp)
Download 50a9946 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 8 2017-12-01T13:06 CET (sv-comp)

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

Trying to find witnesses for program (bb493101aba486c02b83eec146067430a253dc574b61bbcd4c41584f28101760, sv-benchmarks/c/ldv-regression/test26_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test26_false-unreach-call_true-termination.c, bb493101aba486c02b83eec146067430a253dc574b61bbcd4c41584f28101760
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/bb493101aba486c02b83eec146067430a253dc574b61bbcd4c41584f28101760.json

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