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/test07_true-unreach-call_true-termination.c
programSHA ed62a3960fcb91462d8831913be0ced139b26809c83ffd5c248763131de7f92a
witnessName results-verified/pesco.2018-12-06_1244.logfiles/sv-comp19_prop-reachsafety.test07_true-unreach-call_true-termination.c.files/witness.graphml
witnessSHA 8a72b52e83f49d5acb012b6e82331ef344f5b474d5ef2dc3b95ca408a3a1d390

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-07T22:45:32+01:00
producer CPAchecker 1.7-svn b8d6131600+
program-sha256 ed62a3960fcb91462d8831913be0ced139b26809c83ffd5c248763131de7f92a
programfile ../../sv-benchmarks/c/ldv-regression/test07_true-unreach-call_true-termination.c
programhash ed62a3960fcb91462d8831913be0ced139b26809c83ffd5c248763131de7f92a
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/8a72b52e83f49d5acb012b6e82331ef344f5b474d5ef2dc3b95ca408a3a1d390.graphml
witness-sha256 8a72b52e83f49d5acb012b6e82331ef344f5b474d5ef2dc3b95ca408a3a1d390
witness-size 5254
witness-type correctness_witness

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

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a993ea4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T22:55 CET (comp)
Download 0897dd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:24:38+01:00 Download 97aa2c4
Download da85b04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:16:21+01:00 Download 2aa6935
Download 5579902 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:09:46+01:00 Download 2b0f04b
Download 63ecb93 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:02:28+01:00 Download 0a31417
Download 5163290 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T00:37:09+01:00 Download 5b7cc0d
Download 753fbbd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T23:46:07+01:00 Download 6a6ecd9
Download 368eddf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T23:39:19+01:00 Download 94c0ebd
Download a5b17a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T19:46:15+01:00 Download 2267220
Download f176e78 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-06T02:03:04+01:00 Download 75bf34b
Download 9ae1e1b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-05T19:13:44+01:00 Download f6a49f8
Download 4073774 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 31500de
Download a270473 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-04T02:07:40+01:00 Download a993ea4
Download 3f1cfa4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-11-30T19:13:35+01:00 Download 1ebcf63
Download 455fe34 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-11-30T16:46:06+01:00 Download 4683d80
Download 4683d80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 5 2019-11-29T20:13:05+01:00
Download 5b7cc0d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 5 2019-12-07T20:16:55+01:00
Download 2b0f04b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 5 2019-11-30T23:53:06+01:00
Download 2cfd4a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:20 CET (comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4956b52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T10:38 CET (sv-comp)
Download 51d1d9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T14:09:45
Download 868f8c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T15:34 CET (sv-comp)
Download 8a72b52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-07T22:45:32+01:00
Download 9fc0329 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T20:02:56+01:00 Download d47cd78
Download 218f25b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T10:31:30+01:00 Download bef6991
Download 25de933 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:17:44+01:00 Download fc216e6
Download 11b74fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T19:54:11+01:00 Download b44cf0a
Download eaf57d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T17:21:37+01:00 Download 1ca58c2
Download 70780d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T23:16:10+01:00 Download 4956b52
Download 9c60d37 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T21:08:47+01:00 Download 51d1d9d
Download 0addc93 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T06:25:35+01:00 Download 8a72b52
Download 9bbc3cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T04:26:25+01:00 Download 8e9989d
Download 8b59f2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T02:09:14+01:00 Download bef6991
Download 4ad0600 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T17:22:21+01:00 Download 5bc3922
Download 9d2f1cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T16:38:15+01:00 Download 868f8c2
Download 3be58fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T08:11:57+01:00 Download c634b44
Download 5f68731 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 7b4edd0
Download 0417206 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T08:51:12+01:00 Download bd08ac5
Download 772c3e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T08:28:18+01:00 Download 865ff3a
Download f254b84 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T08:14:06+01:00 Download db318ab
Download bd08ac5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T03:47:45+01:00
Download bbd3011 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T09:22 CET (sv-comp)
Download cc9fb49 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T09:57 CET (sv-comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f50ca0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Forester 6 2017-12-01T18:09 CET (sv-comp)
Download 5bc3922 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:37 CET (sv-comp)
Download 5560be2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 9 2017-12-03T03:30Z
Download c2500f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T07:06 CET (sv-comp)
Download c634b44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness PredatorHP 4 2017-12-01T20:39 CET (sv-comp)
Download 19087fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 9 2017-12-02T18:04Z
Download 3522561 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T01:27:11.644658
Download eb5086f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T13:37:09.150337
Download b74cde9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T19:24:30.670347
Download b9711e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T14:44:46.174273
Download 57f20e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 5 2017-12-01T16:23 CET (sv-comp)
Download 05bafb5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 5 2017-12-02T21:12:07+01:00
Download 216dfbc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-11-30T18:40:27+01:00
Download c3e55ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T07:06:19+01:00 7578c2f
Download ee7afb7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T04:01:43+01:00 5d1821a
Download 89f5e83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T02:20:04+01:00 a87f96d
Download 22ecdc5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T00:32:56+01:00 6294d8d
Download 5dbeb71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T20:34:48+01:00 b34bdee
Download 57ff002 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T15:02:52+01:00 56d9451
Download 01adee8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T08:59:31+01:00 af3fdd3
Download f710c67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T00:14:54+01:00 b8cb852
Download d436c87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T22:27:45+01:00 3838da5
Download 851d9d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T21:03:54+01:00 4c09a7a
Download da4c17d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T08:13:30+01:00 0a9cbfe
Download 9decd7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T07:15:19+01:00 c9a0bb1
Download c87ef08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T06:49:59+01:00 8b583ee
Download 2328080 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T06:46:29+01:00 d8e041d
Download 8a05be9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T06:42:10+01:00 d3fb337
Download 7ff3c5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T06:22:30+01:00 99bfee1
Download f43784d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-11-30T13:53:06+01:00
Download 41c2e04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 12 2017-11-30T18:54:35+01:00
Download 9957026 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T20:53:52+01:00
Download d4095ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 5 2017-12-02T02:31:05+01:00
Download a4d9aac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 6 2017-11-30T13:19 CET (sv-comp)
Download 3c08238 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 9 2017-12-02T06:36Z
Download 88e31dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 11 2017-11-30T21:53 CET (sv-comp)
Download d1ce500 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 6 2017-12-01T13:34 CET (sv-comp)
Download 6fc3bde Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 11 2017-12-01T16:21 CET (sv-comp)

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

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

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

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