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/test30_false-unreach-call_true-termination.c
programSHA 00eccf3e88d698bf3100477fb06465e4f6064f0ac30946cf8af1aea4e1eae9ae
witnessName results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-reachsafety.test30_false-unreach-call_true-termination.c.files/witness.graphml
witnessSHA b98a32f7db2842dbf2c5ef04fbabe84ab752c810042fd53167ce5316c6a95bee

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-05T17:44:00.809357
producer DepthK v3.0
programfile /tmp/vcloud-vcloud-master/worker/working_dir_69e769c6-bd30-44c5-bb84-7301a938cd67/sv-benchmarks/c/ldv-regression/test30_false-unreach-call_true-termination.c
programhash dbf4229fc71e086a20df7dc549a8cc43d35a83d5
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/b98a32f7db2842dbf2c5ef04fbabe84ab752c810042fd53167ce5316c6a95bee.graphml
witness-sha256 b98a32f7db2842dbf2c5ef04fbabe84ab752c810042fd53167ce5316c6a95bee
witness-size 3682
witness-type violation_witness

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

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

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

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

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

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

Found 21 witnesses for program sv-benchmarks/c/ldv-regression/test30_false-unreach-call_true-termination.c, 00eccf3e88d698bf3100477fb06465e4f6064f0ac30946cf8af1aea4e1eae9ae
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/00eccf3e88d698bf3100477fb06465e4f6064f0ac30946cf8af1aea4e1eae9ae.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 256b871 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-02 01:29:40
Download 0f2f33a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 4 2019-12-03T23:05 CET (comp)
Download 481c7e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T21:56:32+01:00 Download 3e8e62f
Download f6cde2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T21:45:01+01:00 Download a87f13a
Download 1541212 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T21:09:31+01:00 Download 256b871
Download e921244 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:55:00+01:00 Download eb903fa
Download d6c57e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:44:26+01:00 Download bd1c3d9
Download d428356 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T01:51:37+01:00 Download 63ffd75
Download 9079682 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T00:27:07+01:00 Download 59bb7e4
Download 197982a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T00:06:05+01:00 Download fbebe41
Download 6af73a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T21:13:23+01:00 Download f180df7
Download 870975f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-06T02:37:57+01:00 Download bb886f6
Download 4795893 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-05T20:20:25+01:00 Download ddd56eb
Download 7222a0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-04T02:58:22+01:00 Download 0f2f33a
Download b041894 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-03T08:56:46+01:00 Download a51b95c
Download 7cb1b2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-03T08:08:35+01:00 Download 6ed567d
Download 6ed567d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 5 2019-11-30T12:07:36+01:00
Download 63ffd75 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 5 2019-12-07T12:27:14+01:00
Download a87f13a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 5 2019-12-01T12:08:24+01:00
Download ae9c8c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-05T19:34:19+01:00 Download 71a87cf
Download 121d02b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T21:44 CET (comp)

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

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

Found 27 witnesses for program sv-benchmarks/c/ldv-regression/test30_false-unreach-call_true-termination.c, 00eccf3e88d698bf3100477fb06465e4f6064f0ac30946cf8af1aea4e1eae9ae
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/00eccf3e88d698bf3100477fb06465e4f6064f0ac30946cf8af1aea4e1eae9ae.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ff49a51 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T05:46 CET (sv-comp)
Download 49d70d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 3 2018-12-08T04:54:16
Download 39961e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 5 2018-12-07T01:34 CET (sv-comp)
Download 98961e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 5 2018-12-10T17:55:57+01:00
Download d4ff488 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-08T00:40:06+01:00
Download 292f21c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-10T20:36:34+01:00 Download 98961e6
Download 2510249 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-10T10:48:46+01:00 Download 60b8f78
Download 7465ffa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:53:05+01:00 Download 89f9441
Download fd0eb18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:37:16+01:00 Download e2d3dd1
Download 3f4d693 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:30:36+01:00 Download f98eed8
Download 5b42204 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T17:59:03+01:00 Download c0377e2
Download f71551e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T23:44:47+01:00 Download ff49a51
Download 97fde07 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T22:11:11+01:00 Download 49d70d2
Download 30170b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T09:03:28+01:00 Download d4ff488
Download 227d4ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T04:56:06+01:00 Download db9fdb9
Download 06a74cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T04:26:23+01:00 Download 60b8f78
Download c32eee2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T17:29:32+01:00 Download 39961e8
Download b814c75 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T09:19:07+01:00 Download 9bc37fd
Download 08ee0d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T01:23:46+01:00 Download 0a9a56d
Download 797755c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T10:17:47+01:00 Download b98a32f
Download b8404b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:48:05+01:00 Download 6c5890b
Download 6c5890b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-05T10:36:55+01:00
Download c1ede46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:41:49+01:00 Download 49f226b
Download 182c315 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:16:37+01:00 Download da6aeb3
Download 5f28446 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:14:56+01:00 Download 24a8abf
Download 2bee554 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T11:07 CET (sv-comp)
Download bb94a6b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T01:58 CET (sv-comp)

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

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

Found 21 witnesses for program sv-benchmarks/c/ldv-regression/test30_false-unreach-call_true-termination.c, 00eccf3e88d698bf3100477fb06465e4f6064f0ac30946cf8af1aea4e1eae9ae
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/00eccf3e88d698bf3100477fb06465e4f6064f0ac30946cf8af1aea4e1eae9ae.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c9b9c52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 7 2017-12-02T23:18Z
Download 8414cf8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T14:54 CET (sv-comp)
Download 9bc37fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness PredatorHP 4 2017-12-01T20:31 CET (sv-comp)
Download 6969117 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 4 2017-12-01T20:14 CET (sv-comp)
Download 10df3c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 6 2017-12-02T07:03Z
Download 8c5914a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T00:01:53.834950
Download 5ffd54d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T10:12:29.818380
Download fe76cdc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-12-01T19:43 CET (sv-comp)
Download 889884f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-12-01T04:45 CET (sv-comp)
Download 038511c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 5 2017-12-02T23:07:35+01:00
Download f1ec9b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-11-30T21:13:00+01:00
Download df966e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 8 2017-11-30T21:35:35+01:00
Download 68921a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 4 2017-12-01T01:21:49+01:00
Download a22c584 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-01T20:11:28+01:00
Download 6de9fcc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 5 2017-12-01T02:26 CET (sv-comp)
Download 6611607 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 6 2017-12-02T13:51Z
Download 49f226b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 3 2017-11-30T23:57 CET (sv-comp)
Download 644eded Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T00:45:00.742850
Download 21336dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T11:29:07.521943
Download d01e714 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 5 2017-12-01T13:48 CET (sv-comp)
Download c0c4d72 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 10 2017-12-01T13:13 CET (sv-comp)

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

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

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

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