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/test21_true-unreach-call_true-termination.c
programSHA 56fb3c2902b50b4a07789a84781b970c839acf0b08754ac3579d7159d4dc5340
witnessName results-verified/esbmc-incr.2017-12-01_0849.logfiles/sv-comp18.test21_true-unreach-call_true-termination.c.files/witness.graphml
witnessSHA 8ffa2d2006249f5ac6ad16ea3561ed3ba2882416ed35f2cb2fc542fef7ff0312

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/8ffa2d2006249f5ac6ad16ea3561ed3ba2882416ed35f2cb2fc542fef7ff0312.json

Key Value
architecture 32bit
creationtime 2017-12-01T10:21:56.867123
producer ESBMC 4.6.0 incr
program-sha256 56fb3c2902b50b4a07789a84781b970c839acf0b08754ac3579d7159d4dc5340
programfile ../../sv-benchmarks/c/ldv-regression/test21_true-unreach-call_true-termination.c
programhash e96ea2b5694d083c4ab21538f2478ac793ab7d6e
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/8ffa2d2006249f5ac6ad16ea3561ed3ba2882416ed35f2cb2fc542fef7ff0312.graphml
witness-sha256 8ffa2d2006249f5ac6ad16ea3561ed3ba2882416ed35f2cb2fc542fef7ff0312
witness-size 3412
witness-type correctness_witness

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6810c0a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T01:05 CET (comp)
Download a337213 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-11T20:28:31+01:00 Download cc25ce1
Download 0a3a17a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-11T20:21:57+01:00 Download 2690b75
Download 4cd8b0d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-11T20:17:33+01:00 Download 9c1a622
Download d87e11d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-11T20:02:54+01:00 Download a291351
Download abd140f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-08T00:50:39+01:00 Download c1b258d
Download 7571a2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-07T23:44:43+01:00 Download f343184
Download 9fc2375 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-07T23:36:19+01:00 Download 6108689
Download 335d9a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-07T19:46:48+01:00 Download ac74956
Download 5a8be5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-06T01:50:29+01:00 Download 311e7b9
Download b772183 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-05T19:12:49+01:00 Download 009b041
Download ed3b705 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-05T19:02:59+01:00 Download 1a20b9a
Download 5be3abf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-12-04T02:07:56+01:00 Download 6810c0a
Download 97f3d9b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-11-30T19:53:09+01:00 Download 0fbc746
Download 5dbfdb1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 7 2019-11-30T17:10:41+01:00 Download 261c4c9
Download 261c4c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 7 2019-11-29T20:30:47+01:00
Download c1b258d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 7 2019-12-07T15:53:37+01:00
Download 9c1a622 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 7 2019-12-01T19:09:40+01:00
Download 126f138 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:23 CET (comp)

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

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

Found 21 witnesses for program sv-benchmarks/c/ldv-regression/test21_true-unreach-call_true-termination.c, 56fb3c2902b50b4a07789a84781b970c839acf0b08754ac3579d7159d4dc5340
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/56fb3c2902b50b4a07789a84781b970c839acf0b08754ac3579d7159d4dc5340.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download af15f6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T14:37 CET (sv-comp)
Download 37307f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T10:47:23
Download 4491ecd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T05:21 CET (sv-comp)
Download 5421b33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-10T20:02:23+01:00 Download 781927e
Download 76dd797 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:27:37+01:00 Download 75bfd95
Download 4411c13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T20:04:24+01:00 Download 1b7a27b
Download b672217 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-09T19:56:39+01:00 Download 139e600
Download ee348c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-08T23:20:09+01:00 Download af15f6e
Download ff4bb22 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-08T21:44:44+01:00 Download 37307f2
Download 65ff7bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-08T03:02:29+01:00 Download 70d2dfd
Download 7285047 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-07T17:45:52+01:00 Download 50d18c6
Download ab23510 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-07T16:38:16+01:00 Download 4491ecd
Download 3e10aeb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-07T08:11:15+01:00 Download c4a854e
Download 695e9a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:28:20+01:00 Download 3d4f638
Download dc8a07c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T09:00:19+01:00 Download 98db4c8
Download 88f7ab4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T08:25:55+01:00 Download 19d0877
Download 929f109 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T07:57:57+01:00 Download 8307081
Download e5ff881 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T07:32:47+01:00 Download 24fb0e1
Download 98db4c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 7 2018-12-06T01:03:16+01:00
Download 7cf4ef5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T07:52 CET (sv-comp)
Download aa17846 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T15:33 CET (sv-comp)

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

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

Found 37 witnesses for program sv-benchmarks/c/ldv-regression/test21_true-unreach-call_true-termination.c, 56fb3c2902b50b4a07789a84781b970c839acf0b08754ac3579d7159d4dc5340
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/56fb3c2902b50b4a07789a84781b970c839acf0b08754ac3579d7159d4dc5340.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 50d18c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:57 CET (sv-comp)
Download a5bdeb2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 12 2017-12-03T04:38Z
Download 759a716 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T06:13 CET (sv-comp)
Download c4a854e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness PredatorHP 4 2017-12-01T20:37 CET (sv-comp)
Download db0af99 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 11 2017-12-02T16:31Z
Download a67bcdb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T00:19:10.503776
Download abc738f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T10:22:00.222666
Download d083812 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T19:18:13.710871
Download 8ffa2d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T10:21:56.867123
Download 6bfdd77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 6 2017-12-01T19:11 CET (sv-comp)
Download 5f44847 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 7 2017-12-03T02:42:32+01:00
Download fac1ba2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T04:35:39+01:00
Download 706859f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-03T07:05:31+01:00 9d7dd32
Download 619a89e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-03T04:08:31+01:00 9eb2f21
Download adcbb01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-03T02:53:38+01:00 c8d4144
Download 89604f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-03T01:20:00+01:00 d4c787c
Download ea27037 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-02T20:03:57+01:00 409cbd4
Download 069965b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-02T15:19:17+01:00 7b28561
Download 239f17d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-02T07:37:09+01:00 d743ca6
Download 152b26b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-02T00:04:29+01:00 d666d54
Download ec1d757 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T22:34:42+01:00 0346069
Download 1537e15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T21:03:56+01:00 db33aa5
Download 58dcf61 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T08:13:55+01:00 6657be2
Download bbd8c0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T06:30:32+01:00 e156120
Download f20448f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T05:15:31+01:00 4781ee5
Download 2fb8338 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T05:07:30+01:00 2d2cfd1
Download f380951 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T04:42:41+01:00 4d1845c
Download a713f56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-12-01T04:40:06+01:00 dcb51cc
Download 33ea48a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 7 2017-11-30T19:28:43+01:00
Download dd1d6b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 14 2017-12-01T02:32:03+01:00
Download bef22db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 7 2017-11-30T19:01:26+01:00
Download ab6ac97 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 8 2017-12-02T13:48:47+01:00
Download aa9b5c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 6 2017-11-30T17:33 CET (sv-comp)
Download ecb2759 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 12 2017-12-02T14:51Z
Download a56d5e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 15 2017-11-30T15:24 CET (sv-comp)
Download 399cf40 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 6 2017-12-01T13:20 CET (sv-comp)
Download d5f6cab Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 15 2017-12-01T12:39 CET (sv-comp)

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

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

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

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