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/float-benchs/nan_float_range_true-unreach-call_true-termination.c
programSHA 52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218
witnessName results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.nan_float_range_true-unreach-call_true-termination.c.files/witness.graphml
witnessSHA c916a7f5c66099b3ba74b45d5d4a0ac2b9b58b535c578f38493ac331bf61d366

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-03T00:28:28+01:00
producer CPAchecker 1.6.1-svn
program-sha256 52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218
programfile /home/benchexec/ar_abs_temp/nan_float_range_true_unreach_call_true_termination_c.c
programhash 64c6d061d6a52be18c2dbf1f223acaf24ab6149e
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/c916a7f5c66099b3ba74b45d5d4a0ac2b9b58b535c578f38493ac331bf61d366.graphml
witness-sha256 c916a7f5c66099b3ba74b45d5d4a0ac2b9b58b535c578f38493ac331bf61d366
witness-size 4767
witness-type correctness_witness

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

Trying to find witnesses for program (52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218, sv-benchmarks/c/float-benchs/nan_float_range_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/nan_float_range_true-unreach-call_true-termination.c, 52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218.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 (52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218, sv-benchmarks/c/float-benchs/nan_float_range_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/nan_float_range_true-unreach-call_true-termination.c, 52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218.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 (52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218, sv-benchmarks/c/float-benchs/nan_float_range_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/nan_float_range_true-unreach-call_true-termination.c, 52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218.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 (52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218, sv-benchmarks/c/float-benchs/nan_float_range_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/nan_float_range_true-unreach-call_true-termination.c, 52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218.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 (52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218, sv-benchmarks/c/float-benchs/nan_float_range_true-unreach-call_true-termination.c).

Found 17 witnesses for program sv-benchmarks/c/float-benchs/nan_float_range_true-unreach-call_true-termination.c, 52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b4c607e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-03T23:22 CET (comp)
Download 49d6a67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:20:52+01:00 Download dd6a4e5
Download b9be552 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:13:22+01:00 Download ab0e43b
Download 9e6f6ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:02:26+01:00 Download 2cb9f9b
Download f0992ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T00:49:50+01:00 Download 7a3e9c6
Download a746835 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T23:47:59+01:00 Download af56a24
Download c9d4237 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T23:36:40+01:00 Download 313d88f
Download 85b896f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T19:43:10+01:00 Download 2615e05
Download 2bfe21b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-05T19:13:16+01:00 Download 683673c
Download 882e77a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-05T19:02:56+01:00 Download 176f7e2
Download 863820b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-04T02:07:41+01:00 Download b4c607e
Download 41da4ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-11-30T19:56:29+01:00 Download a9c3aa3
Download 699def6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-11-30T16:12:10+01:00 Download 4486107
Download 4486107 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 5 2019-11-29T23:33:51+01:00
Download 7a3e9c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 5 2019-12-07T12:08:15+01:00
Download ab0e43b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 5 2019-11-30T21:17:24+01:00
Download af56a24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness BRICK 3 2019-12-07T21:39:06Z

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

Trying to find witnesses for program (52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218, sv-benchmarks/c/float-benchs/nan_float_range_true-unreach-call_true-termination.c).

Found 18 witnesses for program sv-benchmarks/c/float-benchs/nan_float_range_true-unreach-call_true-termination.c, 52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e20631e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T15:44:09
Download 5366cba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T02:58 CET (sv-comp)
Download 38611e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-07T14:32:06+01:00
Download 03fbcc8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T20:17:05+01:00 Download df23d58
Download 51a7c50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:20:30+01:00 Download 8eb21cf
Download f7ddcfc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:05:45+01:00 Download 57204e6
Download 4f752f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-09T19:54:38+01:00 Download f69a58b
Download 8206b60 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T21:26:08+01:00 Download e20631e
Download e32427c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T06:20:16+01:00 Download 38611e8
Download d93419a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-08T03:10:32+01:00 Download b13dc82
Download 1d142c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T17:46:04+01:00 Download fa1cf10
Download 2d2ea56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-07T16:38:36+01:00 Download 5366cba
Download bef1dcb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:28:37+01:00 Download 5baa6cc
Download 202fe6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T08:45:42+01:00 Download ff29b8e
Download eb113dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T08:28:12+01:00 Download 5839a07
Download bf1a166 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T08:25:03+01:00 Download 3a5d643
Download e732ba0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T08:09:03+01:00 Download daceeff
Download ff29b8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T01:45:38+01:00

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

Trying to find witnesses for program (52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218, sv-benchmarks/c/float-benchs/nan_float_range_true-unreach-call_true-termination.c).

Found 26 witnesses for program sv-benchmarks/c/float-benchs/nan_float_range_true-unreach-call_true-termination.c, 52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7f46814 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 5 2017-12-03T04:06Z
Download 731a808 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 5 2017-12-02T10:00Z
Download a00ebf0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T20:23:18.988334
Download 6e3626a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T16:32:00.725172
Download c916a7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 5 2017-12-03T00:28:28+01:00
Download fa07931 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-11-30T21:36:58+01:00
Download dd8346f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T07:01:13+01:00 ae22ae3
Download a251dc6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T04:21:46+01:00 c023569
Download 2898761 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T02:41:50+01:00 0d39148
Download e775d42 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T01:10:59+01:00 8860e0c
Download 200c7d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T14:35:40+01:00 3bacee4
Download d061b3d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T07:00:23+01:00 248cd64
Download 6aebcfc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T22:24:34+01:00 f7b2beb
Download 1973c19 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T08:13:09+01:00 3ca8cdb
Download 341432b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T05:51:18+01:00 6d44762
Download 66693c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T05:48:42+01:00 e9c2cfb
Download d9d28a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T05:27:29+01:00 7647032
Download 7cb641a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T05:19:17+01:00 8733dc3
Download 0e520ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T04:39:50+01:00 d6c2595
Download 4aa1230 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-11-30T14:50:44+01:00
Download ff20835 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 7 2017-11-30T15:59:28+01:00
Download 45d8306 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 5 2017-12-01T03:33:46+01:00
Download ade1f54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 5 2017-12-02T06:32:56+01:00
Download 56cb85d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 4 2017-11-30T11:54 CET (sv-comp)
Download 82fad36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 5 2017-12-02T06:25Z
Download 67f48a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 7 2017-11-30T18:00 CET (sv-comp)

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

Trying to find witnesses for program (52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218, sv-benchmarks/c/float-benchs/nan_float_range_true-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/float-benchs/nan_float_range_true-unreach-call_true-termination.c, 52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/52429e7bb282dcb4673791195d34a68789cb08bdd9301c6e72972cae020ef218.json

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