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/test30_true-unreach-call_true-termination.c
programSHA dbcca5c796b0265c83a038b1d35dd1521aa2dc99bca5036ea34be15cda581b02
witnessName results-validated/cpa-seq-validate-correctness-witnesses-uautomizer.2018-12-09_1643.logfiles/sv-comp19_prop-reachsafety.test30_true-unreach-call_true-termination.c.files/witness.graphml
witnessSHA eeccbced01a98e3ac1bdaec3c3133a944e02488fb50115a49a0b0fb282f7d387

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-09T20:08:56+01:00
inputwitnesshash 339a502cd0c746d6243cee473ab0242312cc0557cb9e998a99828005b2d8fcb1
producer CPAchecker 1.7-svn 29852
program-sha256 dbcca5c796b0265c83a038b1d35dd1521aa2dc99bca5036ea34be15cda581b02
programfile ../../sv-benchmarks/c/ldv-regression/test30_true-unreach-call_true-termination.c
programhash dbcca5c796b0265c83a038b1d35dd1521aa2dc99bca5036ea34be15cda581b02
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/eeccbced01a98e3ac1bdaec3c3133a944e02488fb50115a49a0b0fb282f7d387.graphml
witness-sha256 eeccbced01a98e3ac1bdaec3c3133a944e02488fb50115a49a0b0fb282f7d387
witness-size 4699
witness-type correctness_witness

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

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 23da400 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T00:48 CET (comp)
Download b16bd0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:30:51+01:00 Download a53ed23
Download cd4b42c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:14:22+01:00 Download 69482a8
Download 59e3f60 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:08:13+01:00 Download e4d7a25
Download 69d07fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:02:19+01:00 Download d32263a
Download 2046713 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T00:36:25+01:00 Download 8e492ba
Download a038646 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T23:47:06+01:00 Download 10cd663
Download 6e75018 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T23:31:19+01:00 Download 63c9d9e
Download bff4311 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T19:47:09+01:00 Download da28bc6
Download 3a61df5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-06T02:04:17+01:00 Download 9a3bdd2
Download d040304 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-05T19:13:24+01:00 Download 707648c
Download 312c8b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-05T19:03:00+01:00 Download f87590b
Download c75b26e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-04T02:07:41+01:00 Download 23da400
Download a5fbf27 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-11-30T19:37:00+01:00 Download 9d97574
Download 3c08357 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-11-30T17:15:44+01:00 Download aad6678
Download aad6678 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 5 2019-11-29T14:42:18+01:00
Download 8e492ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 5 2019-12-07T15:40:34+01:00
Download e4d7a25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 5 2019-12-01T12:57:34+01:00
Download fbc3593 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:45 CET (comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b053cce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T02:37 CET (sv-comp)
Download 7b7870f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T07:12:36
Download a4c67f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T11:10 CET (sv-comp)
Download f4196e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-06T22:41:03+01:00
Download c11975d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T20:05:32+01:00 Download 4307277
Download d62ee4b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T10:31:11+01:00 Download c6750ca
Download acc071b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:31:50+01:00 Download bb45fd3
Download eeccbce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:08:56+01:00 Download 339a502
Download 957daa3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T19:58:05+01:00 Download b5edfe1
Download a9a56b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T23:23:53+01:00 Download b053cce
Download e687f56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T21:38:24+01:00 Download 7b7870f
Download 13101ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T06:06:57+01:00 Download f4196e5
Download 22e6ad4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T03:41:59+01:00 Download 291d312
Download 68abc0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T02:08:38+01:00 Download c6750ca
Download 0c0ba76 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T16:38:28+01:00 Download a4c67f3
Download aac3cab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T08:52:53+01:00 Download e067837
Download 09719dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:28:28+01:00 Download 1499d8d
Download 36bbd45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T08:53:35+01:00 Download d3784c3
Download a4e1c5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T08:27:47+01:00 Download d384f13
Download ab32ce9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T07:30:42+01:00 Download 354abdc
Download d3784c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-05T20:37:54+01:00
Download 71adef1 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-07T23:01 CET (sv-comp)
Download 93ab383 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T10:42 CET (sv-comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 354abdc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 3 2017-11-30T16:38 CET (sv-comp)
Download 0cb72d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 7 2017-12-03T02:28Z
Download 06b87fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T10:42 CET (sv-comp)
Download e067837 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness PredatorHP 4 2017-12-01T20:31 CET (sv-comp)
Download 1d93019 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 7 2017-12-02T04:04Z
Download af00aa0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T23:39:20.166097
Download 27a4ff8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T08:05:04.906376
Download a48b15b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T12:44:07.682096
Download d1a5060 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T07:49:53.722423
Download 1eac9e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 4 2017-12-01T18:54 CET (sv-comp)
Download bd9aa08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 5 2017-12-03T01:09:40+01:00
Download f3eb375 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-11-30T19:04:55+01:00
Download aaca29f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T07:05:00+01:00 b3c50b4
Download 219f4a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T04:20:56+01:00 a957fa7
Download f0eb5f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T01:52:40+01:00 3083952
Download 70251af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T01:06:01+01:00 5d30052
Download 59c18af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T20:50:45+01:00 cc0d117
Download b4d9bcf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T15:06:59+01:00 231f1c8
Download 26975e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T08:18:48+01:00 a1d3d04
Download 7f87afe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T22:29:33+01:00 df83528
Download a154242 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T21:03:56+01:00 3b312ac
Download 4aac97b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T08:13:56+01:00 e90b57f
Download f2b2df3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T06:34:44+01:00 b4cfbf9
Download 09a39a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T06:28:46+01:00 59f9afc
Download d953ad1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T05:24:27+01:00 f2443ac
Download 4bfe70f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T04:55:13+01:00 6ff6147
Download 97942b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-11-30T19:58:21+01:00
Download a28c261 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 9 2017-11-30T11:53:48+01:00
Download 8a158c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 5 2017-12-01T03:47:41+01:00
Download acace0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 5 2017-12-01T20:03:26+01:00
Download bfaab3e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 4 2017-11-30T15:36 CET (sv-comp)
Download 5551b35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 7 2017-12-02T03:11Z
Download 430c3e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 4 2017-12-01T16:36 CET (sv-comp)
Download b24a370 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 10 2017-12-01T14:57 CET (sv-comp)

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

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

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

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