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/loops/eureka_05_true-unreach-call_true-termination.i
programSHA 3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac
witnessName results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.eureka_05_true-unreach-call_true-termination.i.files/witness.graphml
witnessSHA 25c105d5ba23b04b7d23a5517dafc6c1b315c23e8180d43b38bcb4ada451e5be

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/25c105d5ba23b04b7d23a5517dafc6c1b315c23e8180d43b38bcb4ada451e5be.json

Key Value
architecture 32bit
creationtime 2017-12-01T00:23:11+01:00
producer CPAchecker 1.6.1-svn
program-sha256 3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac
programfile /tmp/vcloud-vcloud-master/worker/working_dir_3fae12bc-d09e-4cb5-ac33-355369ec4e9b/sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i
programhash 34e145a8c3496c7a6f8cda2178ee26349d80aa46
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/25c105d5ba23b04b7d23a5517dafc6c1b315c23e8180d43b38bcb4ada451e5be.graphml
witness-sha256 25c105d5ba23b04b7d23a5517dafc6c1b315c23e8180d43b38bcb4ada451e5be
witness-size 3906
witness-type correctness_witness

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

Trying to find witnesses for program (3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac, sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i, 3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac.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 (3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac, sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i, 3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac.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 (3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac, sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i, 3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac.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 (3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac, sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i, 3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac.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 (3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac, sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i).

Found 16 witnesses for program sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i, 3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 05cc91f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T00:23 CET (comp)
Download efc7aaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T20:19:56+01:00 Download 0052936
Download ddf1cda Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T20:17:54+01:00 Download d29fa52
Download 1fe358e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T20:13:40+01:00 Download 7939dda
Download 3a80ea6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-11T20:03:11+01:00 Download fcb7807
Download 13acdc2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-08T00:36:17+01:00 Download ec4d8d2
Download 8c59699 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-06T01:53:42+01:00 Download 320c40c
Download c253a47 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-05T19:13:01+01:00 Download f8cdd36
Download d3379fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-05T19:03:03+01:00 Download 0655583
Download 122debc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-12-04T02:07:31+01:00 Download 05cc91f
Download 82aaaf4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-11-30T19:37:32+01:00 Download 277d681
Download 4b8e749 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 9 2019-11-30T16:17:35+01:00 Download b93e60b
Download b93e60b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 10 2019-11-30T00:26:32+01:00
Download ec4d8d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 10 2019-12-07T19:58:28+01:00
Download 7939dda Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 10 2019-11-30T23:43:31+01:00
Download 46260d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:01 CET (comp)

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

Trying to find witnesses for program (3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac, sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i).

Found 22 witnesses for program sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i, 3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c3a3cde Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T01:36 CET (sv-comp)
Download 3c1b532 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T07:28:34
Download c30f73f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T07:45 CET (sv-comp)
Download fe4b6b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 10 2018-12-10T18:34:21+01:00
Download 23d0ed1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 10 2018-12-07T03:37:49+01:00
Download cd78482 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-10T20:20:39+01:00 Download fe4b6b9
Download a771e92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-10T10:45:22+01:00 Download d956ccc
Download 3ee8ffc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-09T21:21:17+01:00 Download f1efd01
Download 70b14c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-09T20:05:41+01:00 Download 230edf3
Download f69dbf4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T23:25:11+01:00 Download c3a3cde
Download 18e8399 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T21:46:56+01:00 Download 3c1b532
Download cfd5136 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T05:29:24+01:00 Download 23d0ed1
Download c9217db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T03:34:45+01:00 Download 033e4e9
Download 7ee6ec4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-08T02:19:01+01:00 Download d956ccc
Download fa30956 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-07T17:59:20+01:00 Download 07417c1
Download b692186 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-07T16:53:45+01:00 Download c30f73f
Download a41c9d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:43:02+01:00 Download dbffced
Download c988e7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T09:07:45+01:00 Download 7106966
Download a6695dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 9 2018-12-06T07:40:52+01:00 Download 0eca536
Download 7106966 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-06T06:53:45+01:00
Download 91f6999 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T05:02 CET (sv-comp)
Download 1227a02 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T08:19 CET (sv-comp)

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

Trying to find witnesses for program (3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac, sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i).

Found 36 witnesses for program sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i, 3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 07417c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T23:34 CET (sv-comp)
Download f312912 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 9 2017-12-03T04:17Z
Download 9982fdc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T00:26 CET (sv-comp)
Download e8cfb87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 4 2017-12-01T21:27 CET (sv-comp)
Download 2c0e380 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 16 2017-12-02T20:16Z
Download ef298c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T01:22:27.019807
Download 9b0d9bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T09:29:06.729938
Download 73a8920 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T00:07:50.593942
Download db0f1b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T07:51:23.973832
Download ea98310 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 12 2017-12-01T19:47 CET (sv-comp)
Download c9cb66c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 14 2017-12-02T19:17:29+01:00
Download 25c105d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T00:23:11+01:00
Download 35c4526 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-03T07:16:56+01:00 4e7d314
Download 17f7bef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-03T04:27:21+01:00 1d0888f
Download db62643 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-03T02:53:39+01:00 7d2b8c8
Download 7ed4b5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-03T02:00:26+01:00 0f380d5
Download 86e18c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-02T20:38:50+01:00 5ec6e43
Download c91d858 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-02T15:37:21+01:00 de49114
Download ffe924e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-02T08:20:38+01:00 ac34d84
Download 28fc665 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-02T00:22:12+01:00 400bd1e
Download c41acce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-01T22:40:54+01:00 a1ccd83
Download 5170e0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-01T22:31:55+01:00 3c6da8f
Download 752511c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-01T08:27:32+01:00 0f8b1a0
Download 709f087 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-01T07:06:07+01:00 05a8590
Download e670ca4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-01T05:43:37+01:00 ae1c5ba
Download 23ce00b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-01T05:41:17+01:00 c1db767
Download 4663299 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 9 2017-12-01T05:31:58+01:00 7fc6d40
Download 9e9aa09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 10 2017-12-01T02:39:01+01:00
Download 91d53b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 11 2017-11-30T11:45:31+01:00
Download bb843a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 10 2017-11-30T18:21:13+01:00
Download d490425 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 9 2017-12-01T22:40:53+01:00
Download d5057a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 31 2017-11-30T13:08 CET (sv-comp)
Download dec3eb4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 9 2017-12-02T10:54Z
Download 009cfe8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 98 2017-11-30T20:37 CET (sv-comp)
Download 04778d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 30 2017-12-01T15:19 CET (sv-comp)
Download a8b321c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 16 2017-12-01T11:54 CET (sv-comp)

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

Trying to find witnesses for program (3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac, sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/eureka_05_true-unreach-call_true-termination.i, 3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/3b9deb97da3a2591a9fa8a7bb2ec41c0b2f7ef338066c02ab42170d5d82be3ac.json

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