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_cast-2_true-unreach-call_true-termination.i
programSHA 52255688a7365ccfb034eca17b0fc41b22428b7da5fd67f0cd9d96dbf91339c5
witnessName results-validated/cpa-seq-validate-correctness-witnesses-esbmc-kind.2018-12-08_0216.logfiles/sv-comp19_prop-reachsafety.test_union_cast-2_true-unreach-call_true-termination.i.files/witness.graphml
witnessSHA 12add0b5497fd369c9c7af7745e9a9e89ea7ec2da061335c90b91ab00c38e463

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-08T02:41:06+01:00
inputwitnesshash f56c5bb26bea62e15f66b16141e8bb2a628f79f2e7c2be5637c9ed4bdfdae22d
producer CPAchecker 1.7-svn 29852
program-sha256 52255688a7365ccfb034eca17b0fc41b22428b7da5fd67f0cd9d96dbf91339c5
programfile ../../sv-benchmarks/c/ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i
programhash 52255688a7365ccfb034eca17b0fc41b22428b7da5fd67f0cd9d96dbf91339c5
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/12add0b5497fd369c9c7af7745e9a9e89ea7ec2da061335c90b91ab00c38e463.graphml
witness-sha256 12add0b5497fd369c9c7af7745e9a9e89ea7ec2da061335c90b91ab00c38e463
witness-size 4205
witness-type correctness_witness

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

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

Trying to find witnesses for program (52255688a7365ccfb034eca17b0fc41b22428b7da5fd67f0cd9d96dbf91339c5, sv-benchmarks/c/ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i).

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

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

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

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

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i, 52255688a7365ccfb034eca17b0fc41b22428b7da5fd67f0cd9d96dbf91339c5
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/52255688a7365ccfb034eca17b0fc41b22428b7da5fd67f0cd9d96dbf91339c5.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 '19

Trying to find witnesses for program (52255688a7365ccfb034eca17b0fc41b22428b7da5fd67f0cd9d96dbf91339c5, sv-benchmarks/c/ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i).

Found 25 witnesses for program sv-benchmarks/c/ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i, 52255688a7365ccfb034eca17b0fc41b22428b7da5fd67f0cd9d96dbf91339c5
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/52255688a7365ccfb034eca17b0fc41b22428b7da5fd67f0cd9d96dbf91339c5.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c22c48c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T06:02 CET (sv-comp)
Download 68e0191 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T07:32:22
Download d521c2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T15:43 CET (sv-comp)
Download a743627 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-07T19:44:22+01:00
Download 6da2940 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-10T20:08:35+01:00 Download 469ee75
Download 436575a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-10T10:31:15+01:00 Download 3894ed4
Download 9eeb001 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:33:33+01:00 Download 2885a1b
Download 8f0c65f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T19:58:51+01:00 Download 4d7ce23
Download 0a42b59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T17:23:13+01:00 Download 6185de4
Download 8390f68 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T23:16:22+01:00 Download c22c48c
Download 6f96b8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T21:28:33+01:00 Download 68e0191
Download 11f47ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T06:29:43+01:00 Download a743627
Download 12add0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T02:41:06+01:00 Download f56c5bb
Download 0b197c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T02:04:13+01:00 Download 3894ed4
Download 3f52685 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T17:45:49+01:00 Download f29c232
Download e11f04f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T16:37:55+01:00 Download d521c2c
Download 6452c73 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T08:40:21+01:00 Download 0fd33c6
Download 1fa1971 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:28:20+01:00 Download 9aa0102
Download 0738f09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:00:32+01:00 Download f8eda68
Download 3376cd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:29:59+01:00 Download 72be1b8
Download 02271b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:21:16+01:00 Download f8e5c1b
Download 5f2f195 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T07:05:10+01:00 Download 562b56e
Download f8eda68 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T02:05:08+01:00
Download 36813dc Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T10:37 CET (sv-comp)
Download 8baf298 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T06:42 CET (sv-comp)

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

Trying to find witnesses for program (52255688a7365ccfb034eca17b0fc41b22428b7da5fd67f0cd9d96dbf91339c5, sv-benchmarks/c/ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i).

Found 39 witnesses for program sv-benchmarks/c/ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i, 52255688a7365ccfb034eca17b0fc41b22428b7da5fd67f0cd9d96dbf91339c5
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/52255688a7365ccfb034eca17b0fc41b22428b7da5fd67f0cd9d96dbf91339c5.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f29c232 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T23:32 CET (sv-comp)
Download 09db0f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 5 2017-12-02T19:17Z
Download 325c50e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T13:44 CET (sv-comp)
Download 0fd33c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness PredatorHP 4 2017-12-01T20:51 CET (sv-comp)
Download ac261ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 3 2017-12-01T21:08 CET (sv-comp)
Download 91009fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 5 2017-12-02T23:14Z
Download 1526b8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T21:23:05.407726
Download 1c3e545 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T13:13:19.726998
Download b928e77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T22:50:29.750043
Download 8d73476 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T16:52:32.719630
Download 6466726 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 4 2017-12-01T18:57 CET (sv-comp)
Download f9d1c5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-03T01:57:54+01:00
Download 6755616 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-11-30T20:29:05+01:00
Download 91b13c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T07:01:52+01:00 326578e
Download 307fe6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T04:05:46+01:00 d0a9e3f
Download f80a5bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T01:37:06+01:00 0a0ee97
Download 44280ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T23:45:02+01:00 93e9585
Download 7147e59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T20:45:32+01:00 222067e
Download fbd11ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T15:26:48+01:00 be33d94
Download b52c5af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T09:01:02+01:00 6219a80
Download 528df34 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T00:08:39+01:00 3257c3c
Download 151e823 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T22:29:30+01:00 ac462d2
Download 468ec1e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T22:18:40+01:00 f34b068
Download d40ad67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T21:03:54+01:00 9b721b8
Download 4bc469c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T08:14:03+01:00 ce8b981
Download bea24d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T07:16:39+01:00 087d9a6
Download bf3693d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T06:05:19+01:00 46b4ef9
Download 3487df1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T05:36:02+01:00 27858cb
Download 1d958d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T05:08:50+01:00 ae43d74
Download f529e81 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T04:59:22+01:00 6a0f31e
Download 2a4cf63 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T02:17:24+01:00
Download 58c88ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 7 2017-11-30T21:51:11+01:00
Download ae91f51 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 4 2017-11-30T21:40:13+01:00
Download 4e1f5ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 4 2017-12-02T00:34:42+01:00
Download 40a4639 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 5 2017-11-30T16:13 CET (sv-comp)
Download c8c2e7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 5 2017-12-02T15:32Z
Download c930137 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 7 2017-12-01T03:23 CET (sv-comp)
Download d50debc Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 5 2017-12-01T16:36 CET (sv-comp)
Download ac1c88f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 7 2017-12-01T12:44 CET (sv-comp)

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

Trying to find witnesses for program (52255688a7365ccfb034eca17b0fc41b22428b7da5fd67f0cd9d96dbf91339c5, sv-benchmarks/c/ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i, 52255688a7365ccfb034eca17b0fc41b22428b7da5fd67f0cd9d96dbf91339c5
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/52255688a7365ccfb034eca17b0fc41b22428b7da5fd67f0cd9d96dbf91339c5.json

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