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/test_union_true-termination.c_true-unreach-call.i
programSHA 72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed
witnessName results-verified/divine-explicit.2018-12-10_1000.logfiles/sv-comp19_prop-reachsafety.test_union_true-termination.c_true-unreach-call.i.files/witness.graphml
witnessSHA cf7e878c2cdfdc2950d437e9d850807a321aa8216c9ea19cf17b2bc212107373

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-07T09:24 CET (sv-comp)
memorymodel precise
producer DIVINE 4
programfile ../../sv-benchmarks/c/ldv-regression/test_union_true-termination.c_true-unreach-call.i
programhash d175f2e77aebe63dd05869db0ed17fb7b8bf3540
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/cf7e878c2cdfdc2950d437e9d850807a321aa8216c9ea19cf17b2bc212107373.graphml
witness-sha256 cf7e878c2cdfdc2950d437e9d850807a321aa8216c9ea19cf17b2bc212107373
witness-size 3227
witness-type correctness_witness

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

Trying to find witnesses for program (72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed, sv-benchmarks/c/ldv-regression/test_union_true-termination.c_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test_union_true-termination.c_true-unreach-call.i, 72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed.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 (72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed, sv-benchmarks/c/ldv-regression/test_union_true-termination.c_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test_union_true-termination.c_true-unreach-call.i, 72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed.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 (72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed, sv-benchmarks/c/ldv-regression/test_union_true-termination.c_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test_union_true-termination.c_true-unreach-call.i, 72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed.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 (72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed, sv-benchmarks/c/ldv-regression/test_union_true-termination.c_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test_union_true-termination.c_true-unreach-call.i, 72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed.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 (72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed, sv-benchmarks/c/ldv-regression/test_union_true-termination.c_true-unreach-call.i).

Found 19 witnesses for program sv-benchmarks/c/ldv-regression/test_union_true-termination.c_true-unreach-call.i, 72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7bceb92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T23:29 CET (comp)
Download 508fb73 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:30:41+01:00 Download 7d1f725
Download cc39702 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:13:03+01:00 Download 8ff1eb8
Download 456176c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:08:46+01:00 Download caf2dce
Download 970259c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:02:36+01:00 Download 569a747
Download 9c83869 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-08T00:52:02+01:00 Download f93f282
Download 341d81b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:47:52+01:00 Download cc1558c
Download 65c6804 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:36:12+01:00 Download 7b8d0fd
Download 1e9dac4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T19:42:35+01:00 Download 59d34e1
Download 4e2c23c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-06T02:07:54+01:00 Download d7564db
Download cf405da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:13:32+01:00 Download 29f7b30
Download 318dec2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:03:00+01:00 Download 375ae47
Download b3330e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-04T02:07:51+01:00 Download 7bceb92
Download 8dee5dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-11-30T19:55:52+01:00 Download a89021b
Download 1c024ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-11-30T16:29:22+01:00 Download 791cb69
Download 791cb69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 4 2019-11-30T14:48:34+01:00
Download f93f282 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 4 2019-12-07T13:07:10+01:00
Download caf2dce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 4 2019-12-01T19:26:57+01:00
Download bcfae30 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:26 CET (comp)

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

Trying to find witnesses for program (72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed, sv-benchmarks/c/ldv-regression/test_union_true-termination.c_true-unreach-call.i).

Found 24 witnesses for program sv-benchmarks/c/ldv-regression/test_union_true-termination.c_true-unreach-call.i, 72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e807898 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T01:14 CET (sv-comp)
Download 3376e38 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T16:32:04
Download 3f52541 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T10:19 CET (sv-comp)
Download c704db5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-06T13:11:01+01:00
Download f940ab8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-10T20:13:02+01:00 Download 4c62af7
Download f77ade9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-10T10:31:30+01:00 Download cf7e878
Download f948a0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:14:22+01:00 Download 3875d98
Download 53ce3f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T19:57:12+01:00 Download 6172537
Download 8163fae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T17:13:02+01:00 Download cf545d6
Download ddeb30e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T23:19:49+01:00 Download e807898
Download 1f95bbb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T21:32:16+01:00 Download 3376e38
Download f290384 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T05:51:43+01:00 Download c704db5
Download de93f8f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T03:31:22+01:00 Download 5f036cb
Download cc0a9a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T02:00:16+01:00 Download cf7e878
Download 9a8b72e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T17:44:48+01:00 Download 136f774
Download c42b124 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T16:38:09+01:00 Download 3f52541
Download 19e63eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T08:52:25+01:00 Download 6776b02
Download 5d425ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:29:02+01:00 Download 1b66534
Download 32eb37e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:52:34+01:00 Download 0ff4caf
Download 27abbc5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:02:36+01:00 Download 6e42334
Download 5652fc1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T07:55:22+01:00 Download e4c9de0
Download 0ff4caf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-05T20:52:33+01:00
Download 7d56340 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T11:29 CET (sv-comp)
Download 765278c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T04:10 CET (sv-comp)

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

Trying to find witnesses for program (72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed, sv-benchmarks/c/ldv-regression/test_union_true-termination.c_true-unreach-call.i).

Found 39 witnesses for program sv-benchmarks/c/ldv-regression/test_union_true-termination.c_true-unreach-call.i, 72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 136f774 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T23:03 CET (sv-comp)
Download 388523d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 5 2017-12-02T21:00Z
Download 455ed41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T03:36 CET (sv-comp)
Download 6776b02 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness PredatorHP 4 2017-12-01T20:26 CET (sv-comp)
Download 6be949e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 2 2017-12-01T19:53 CET (sv-comp)
Download b139676 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 5 2017-12-02T12:55Z
Download 54fe680 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T21:35:48.077629
Download ab720d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T10:42:23.156320
Download ae0122f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T18:10:22.973371
Download 83df6ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T18:00:45.218449
Download 680355b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 4 2017-12-01T21:17 CET (sv-comp)
Download 743fb4f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-03T02:57:46+01:00
Download f3b5e98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-11-30T23:22:38+01:00
Download 69bc2cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T07:00:03+01:00 383d2cd
Download c16e394 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T04:08:27+01:00 37042af
Download 670e57e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T02:21:36+01:00 3ee0305
Download 9e8102e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T00:14:40+01:00 d05522e
Download 6a60acc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T20:50:02+01:00 a890c5d
Download f0d9db3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T14:40:44+01:00 f963c5c
Download 0ed061f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T07:20:48+01:00 5dd3589
Download d936f9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T00:11:17+01:00 5250cdd
Download 630b612 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T22:22:55+01:00 5a21a97
Download e669cd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T22:07:20+01:00 b4b671d
Download 4428632 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T21:04:37+01:00 79273df
Download 57f233a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T08:13:53+01:00 d23df5b
Download 18137cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T07:11:36+01:00 8b046dd
Download 0f2bf7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T06:35:45+01:00 44c6368
Download 001dc17 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T05:55:50+01:00 5bfe42c
Download 475876e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T05:29:12+01:00 f9dd6dd
Download a0dedf8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T04:32:13+01:00 7172a98
Download 37f2ad2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T03:43:02+01:00
Download fb5cfde Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 6 2017-11-30T21:44:31+01:00
Download e86f2e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 4 2017-12-01T00:41:17+01:00
Download 0f4c5bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 4 2017-12-01T20:30:54+01:00
Download fb7d28a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 3 2017-11-30T18:38 CET (sv-comp)
Download bc358bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 5 2017-12-02T17:25Z
Download 86e9e5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 6 2017-11-30T21:23 CET (sv-comp)
Download a1efc95 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 3 2017-12-01T19:21 CET (sv-comp)
Download b4e774d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 6 2017-12-01T16:17 CET (sv-comp)

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

Trying to find witnesses for program (72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed, sv-benchmarks/c/ldv-regression/test_union_true-termination.c_true-unreach-call.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test_union_true-termination.c_true-unreach-call.i, 72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/72fcc84a43719dc4e6abfc61e98a04474fc6220e902ed0975c756b8cdb3e68ed.json

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