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/addsub_double_exact_true-unreach-call_true-termination.c
programSHA 3f442989293062a2c04002d472517ab8627237733ecad09a491ca56be11624e0
witnessName results-verified/cbmc.2018-12-04_2248.logfiles/sv-comp19_prop-reachsafety.addsub_double_exact_true-unreach-call_true-termination.c.files/witness.graphml
witnessSHA 508e8727283f3a4b59e9bf8efc69f67f1d649b10a1516475254f76ef351b72af

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-05T14:41 CET (sv-comp)
producer CBMC
programfile ../../sv-benchmarks/c/float-benchs/addsub_double_exact_true-unreach-call_true-termination.c
programhash e20164d66b413fd1e6480d779b873570f1c551b2
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/508e8727283f3a4b59e9bf8efc69f67f1d649b10a1516475254f76ef351b72af.graphml
witness-sha256 508e8727283f3a4b59e9bf8efc69f67f1d649b10a1516475254f76ef351b72af
witness-size 5001
witness-type correctness_witness

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

Trying to find witnesses for program (3f442989293062a2c04002d472517ab8627237733ecad09a491ca56be11624e0, sv-benchmarks/c/float-benchs/addsub_double_exact_true-unreach-call_true-termination.c).

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f1cdd44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T00:16 CET (comp)
Download 090d0c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:17:54+01:00 Download 62edd5a
Download ca2dca6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:17:43+01:00 Download d346160
Download 17404f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-11T20:02:16+01:00 Download 2231957
Download 8e9db91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-08T00:50:12+01:00 Download b1d7dbc
Download 0461083 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:46:27+01:00 Download 93340cd
Download 6448a91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T23:38:14+01:00 Download bca529f
Download 157afc5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-07T19:45:15+01:00 Download 92de694
Download 10f94fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:13:26+01:00 Download 0594db3
Download d37671f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:02:50+01:00 Download 009ee4b
Download e2c1bbe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-04T02:07:26+01:00 Download f1cdd44
Download f5e6be5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-11-30T19:52:03+01:00 Download 1d82e0c
Download 454745a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-11-30T16:17:28+01:00 Download 4232515
Download 4232515 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 4 2019-11-29T19:52:14+01:00
Download b1d7dbc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 4 2019-12-07T19:09:30+01:00
Download d346160 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 4 2019-11-30T21:28:48+01:00
Download 93340cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness BRICK 3 2019-12-07T21:37:53Z

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

Trying to find witnesses for program (3f442989293062a2c04002d472517ab8627237733ecad09a491ca56be11624e0, sv-benchmarks/c/float-benchs/addsub_double_exact_true-unreach-call_true-termination.c).

Found 21 witnesses for program sv-benchmarks/c/float-benchs/addsub_double_exact_true-unreach-call_true-termination.c, 3f442989293062a2c04002d472517ab8627237733ecad09a491ca56be11624e0
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/3f442989293062a2c04002d472517ab8627237733ecad09a491ca56be11624e0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ea03d03 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T01:27 CET (sv-comp)
Download 48ef30b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T05:21:29
Download 040d240 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T15:44 CET (sv-comp)
Download ccb66ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-07T09:31:29+01:00
Download 3566db9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-10T19:35:45+01:00 Download 3497b07
Download ae8e966 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-10T10:30:51+01:00 Download af71ce4
Download 55725d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T20:32:10+01:00 Download 4f73e59
Download 5df06e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T19:58:34+01:00 Download 7a67ab9
Download 15ba3a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-09T17:37:25+01:00 Download 12d87a5
Download 2674879 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T23:21:34+01:00 Download ea03d03
Download a7a916d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T21:42:10+01:00 Download 48ef30b
Download 9573ef8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T07:14:37+01:00 Download ccb66ba
Download cc57032 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T04:18:59+01:00 Download 15c0bf8
Download 8416be2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T01:56:58+01:00 Download af71ce4
Download 69f4b8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T17:45:42+01:00 Download 7e862d7
Download a1f9b15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-07T16:38:07+01:00 Download 040d240
Download b565839 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:28:16+01:00 Download a8e5c87
Download 27f2597 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:45:28+01:00 Download 6896cf0
Download 650f1ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T08:16:42+01:00 Download 508e872
Download 6650846 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T07:47:15+01:00 Download 8c6cd84
Download 6896cf0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T02:15:35+01:00

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

Trying to find witnesses for program (3f442989293062a2c04002d472517ab8627237733ecad09a491ca56be11624e0, sv-benchmarks/c/float-benchs/addsub_double_exact_true-unreach-call_true-termination.c).

Found 30 witnesses for program sv-benchmarks/c/float-benchs/addsub_double_exact_true-unreach-call_true-termination.c, 3f442989293062a2c04002d472517ab8627237733ecad09a491ca56be11624e0
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/3f442989293062a2c04002d472517ab8627237733ecad09a491ca56be11624e0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7e862d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness skink 3 2017-12-01T22:27 CET (sv-comp)
Download 41ace69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Taipan 5 2017-12-03T05:10Z
Download 908bf61 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T06:54 CET (sv-comp)
Download 6c62406 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 5 2017-12-02T19:18Z
Download 4356885 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T20:12:35.797647
Download 941f876 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T11:40:15.279869
Download aa585a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-02T18:26:02+01:00
Download 29ccd59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T04:02:13+01:00
Download 52649dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T06:52:24+01:00 62ea055
Download 64eecbc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T04:11:37+01:00 be07c70
Download 87d88af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-03T02:03:37+01:00 b6de629
Download 6da579f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T23:47:20+01:00 4d2706b
Download 00a7e07 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T20:41:46+01:00 4f38a8e
Download 6be83a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T15:19:06+01:00 a7f3636
Download c9a4c58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-02T07:34:55+01:00 2e4ce12
Download 15655b3 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 9eba433
Download 4adfbc6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T22:30:54+01:00 f6cf8a0
Download a526969 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T08:13:58+01:00 53e445f
Download 3380bba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T07:08:47+01:00 4d7dbfc
Download 71fae6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T06:21:52+01:00 6031243
Download f523c9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T05:14:42+01:00 2445a07
Download 7257a8f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T04:44:18+01:00 cb408bf
Download 91bc2c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T04:31:30+01:00 b564501
Download d696537 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-11-30T11:43:45+01:00
Download 90f1097 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 9 2017-11-30T22:37:06+01:00
Download 98fb1b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 4 2017-11-30T11:47:33+01:00
Download 538af95 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 4 2017-12-01T21:55:15+01:00
Download 65f9a30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 5 2017-12-01T02:56 CET (sv-comp)
Download 2dc3391 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Automizer 5 2017-12-02T14:52Z
Download 03ed520 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 9 2017-11-30T11:39 CET (sv-comp)

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

Trying to find witnesses for program (3f442989293062a2c04002d472517ab8627237733ecad09a491ca56be11624e0, sv-benchmarks/c/float-benchs/addsub_double_exact_true-unreach-call_true-termination.c).

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

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