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/test29_true-unreach-call_true-termination.c
programSHA 202d96d05e02650bf08160c92c59e8df143683e0f949fddedf0b326151e4f066
witnessName results-verified/ukojak.2017-12-02_0233.logfiles/sv-comp18.test29_true-unreach-call_true-termination.c.files/witness.graphml
witnessSHA 279e4d5d2aad0744077945c1b28d2528c78d867d08aeb0be57184a4c29f98907

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/279e4d5d2aad0744077945c1b28d2528c78d867d08aeb0be57184a4c29f98907.json

Key Value
architecture 32bit
creationtime 2017-12-02T15:24Z
producer Kojak
program-sha256 202d96d05e02650bf08160c92c59e8df143683e0f949fddedf0b326151e4f066
programfile /tmp/vcloud-vcloud-master/worker/working_dir_4702d169-26a3-4bd8-9955-54fc45fcc035/sv-benchmarks/c/ldv-regression/test29_true-unreach-call_true-termination.c
programhash 5a0b8f7221e31cc2cda01831098deec15967e67b
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/279e4d5d2aad0744077945c1b28d2528c78d867d08aeb0be57184a4c29f98907.graphml
witness-sha256 279e4d5d2aad0744077945c1b28d2528c78d867d08aeb0be57184a4c29f98907
witness-size 7986
witness-type correctness_witness

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b2699bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T00:23 CET (comp)
Download 7748fa4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:30:53+01:00 Download 537378b
Download baed423 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:21:27+01:00 Download e607ce3
Download d3927cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:12:22+01:00 Download 9fb4511
Download 691c463 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:02:25+01:00 Download 1883a9a
Download c24f03d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T00:36:34+01:00 Download d4be0df
Download a2187e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T23:47:14+01:00 Download 803eedd
Download 5639cd4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T23:40:26+01:00 Download 77fa4d1
Download 1fc7be0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T19:46:13+01:00 Download c3781f9
Download d636865 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-06T01:59:32+01:00 Download 0fe6390
Download c3142d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-05T19:13:21+01:00 Download ac320a5
Download 19aabac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-05T19:02:49+01:00 Download dc6deed
Download 9501305 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-04T02:07:54+01:00 Download b2699bc
Download 96e1f8a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-11-30T19:34:16+01:00 Download 6c2fca6
Download 4e26e9b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-11-30T16:56:55+01:00 Download 45ed408
Download 45ed408 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 5 2019-11-30T14:04:14+01:00
Download d4be0df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 5 2019-12-07T12:21:34+01:00
Download 9fb4511 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 5 2019-12-01T06:53:54+01:00
Download 5236407 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:49 CET (comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 530aa96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T14:23 CET (sv-comp)
Download 79b142c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T11:21:44
Download 31c04be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-06T22:25 CET (sv-comp)
Download 98ed777 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-08T02:35:25+01:00
Download dea6649 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T19:48:19+01:00 Download 68f88f2
Download 1240393 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:16:56+01:00 Download 6278f93
Download 65d44c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:08:16+01:00 Download 4f8e0d2
Download defffd2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T19:40:50+01:00 Download c7a2940
Download ce61b81 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T23:07:18+01:00 Download 530aa96
Download c384bce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T21:09:22+01:00 Download 79b142c
Download 38fb2ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T07:05:43+01:00 Download 98ed777
Download daf43dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T02:25:20+01:00 Download 6be8a31
Download 9807ced Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T02:22:34+01:00 Download e92b0ae
Download a7cb102 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T16:37:40+01:00 Download 31c04be
Download a44c2d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T08:52:21+01:00 Download c03278c
Download 55163c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:29:03+01:00 Download 73841c6
Download 5ddc401 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T08:56:23+01:00 Download fd9e520
Download c648339 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T08:19:09+01:00 Download dce6f01
Download ee88fcb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T07:58:52+01:00 Download d9dae69
Download a428538 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T07:49:13+01:00 Download 1758e1c
Download fd9e520 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-05T22:09:34+01:00
Download f2d82cf Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T11:30 CET (sv-comp)
Download 67e0f36 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T04:27 CET (sv-comp)

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

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

Found 35 witnesses for program sv-benchmarks/c/ldv-regression/test29_true-unreach-call_true-termination.c, 202d96d05e02650bf08160c92c59e8df143683e0f949fddedf0b326151e4f066
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/202d96d05e02650bf08160c92c59e8df143683e0f949fddedf0b326151e4f066.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download df61489 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 8 2017-12-02T19:49Z
Download 825913b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T07:57 CET (sv-comp)
Download c03278c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness PredatorHP 4 2017-12-01T20:39 CET (sv-comp)
Download 279e4d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 8 2017-12-02T15:24Z
Download 14b8ab2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T22:10:09.981018
Download 12ad0c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T13:10:19.800182
Download 0a86df3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T22:56:29.706415
Download 8c3b368 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T12:11:17.493630
Download 819e303 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 5 2017-12-01T15:17 CET (sv-comp)
Download 012089c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 5 2017-12-03T02:06:09+01:00
Download cb46896 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T06:37:53+01:00
Download 21ce4e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T06:52:11+01:00 5e86c29
Download 6fabedd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T04:02:37+01:00 8bc9e50
Download 133cbbc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T02:35:46+01:00 efa44b8
Download 377bd67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T01:23:18+01:00 b16ab4d
Download 8cca4e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T20:10:50+01:00 aff0ef5
Download 3a5a7b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T15:21:55+01:00 3f9c8fb
Download e1b4bab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T07:39:49+01:00 decd98c
Download 114711e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T22:33:53+01:00 31a4173
Download 43ef63f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T21:04:01+01:00 9e93a65
Download 3f3125e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T08:13:34+01:00 a5c0454
Download 00a9f5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T07:08:49+01:00 6515b3f
Download d1568ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T07:00:19+01:00 62e55fd
Download 02f2bea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T06:36:16+01:00 d2f2fb7
Download 54eb9fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T05:57:10+01:00 a648066
Download 61e93c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T05:31:46+01:00 6dd89e7
Download 1cbeb1d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T03:23:59+01:00
Download 8a9e2e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 11 2017-11-30T12:06:21+01:00
Download 46f64df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 5 2017-12-01T03:52:54+01:00
Download 1d59d9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 5 2017-12-02T00:48:59+01:00
Download 42b6e52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 5 2017-12-01T00:11 CET (sv-comp)
Download cfc4f63 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 8 2017-12-02T00:40Z
Download 55e3799 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 9 2017-11-30T23:09 CET (sv-comp)
Download e3d73ae Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 5 2017-12-01T14:20 CET (sv-comp)
Download f34609c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2017-12-01T16:07 CET (sv-comp)

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

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

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

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