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/eca-rers2012/Problem01_label57_false-unreach-call_false-termination.c
programSHA 1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0
witnessName results-verified/esbmc-incr.2017-12-01_0849.logfiles/sv-comp18.Problem01_label57_false-unreach-call_false-termination.c.files/witness.graphml
witnessSHA 50966e9454e48f9ea6bf6d1dcbdaf34c7af44d0c1b2ee562fc700ba1180b17e2

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-01T09:18:53.372537
producer ESBMC 4.6.0 incr
program-sha256 1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0
programfile ../../sv-benchmarks/c/eca-rers2012/Problem01_label57_false-unreach-call_false-termination.c
programhash 00372dd9706fe72201713f336fbc903974e88ef8
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/50966e9454e48f9ea6bf6d1dcbdaf34c7af44d0c1b2ee562fc700ba1180b17e2.graphml
witness-sha256 50966e9454e48f9ea6bf6d1dcbdaf34c7af44d0c1b2ee562fc700ba1180b17e2
witness-size 4804
witness-type violation_witness

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

Trying to find witnesses for program (1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0, sv-benchmarks/c/eca-rers2012/Problem01_label57_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label57_false-unreach-call_false-termination.c, 1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0.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 (1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0, sv-benchmarks/c/eca-rers2012/Problem01_label57_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label57_false-unreach-call_false-termination.c, 1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0.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 (1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0, sv-benchmarks/c/eca-rers2012/Problem01_label57_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label57_false-unreach-call_false-termination.c, 1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0.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 (1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0, sv-benchmarks/c/eca-rers2012/Problem01_label57_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label57_false-unreach-call_false-termination.c, 1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0.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 (1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0, sv-benchmarks/c/eca-rers2012/Problem01_label57_false-unreach-call_false-termination.c).

Found 18 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label57_false-unreach-call_false-termination.c, 1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c3a18f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2019-12-01 04:59:16
Download c7fd170 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 70 2019-12-03T22:44 CET (comp)
Download 8618b8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 205 2019-12-11T21:51:35+01:00 Download abe3ea7
Download e26ebde Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 204 2019-12-11T21:09:29+01:00 Download c3a18f7
Download 2ab037c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 205 2019-12-11T20:54:38+01:00 Download a8571fc
Download 5a8753b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 205 2019-12-11T20:44:50+01:00 Download 461a9b4
Download 282372f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 206 2019-12-08T01:51:29+01:00 Download 48cb673
Download 0eb866e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 258 2019-12-04T02:58:21+01:00 Download c7fd170
Download b3dfabf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 205 2019-12-03T08:10:05+01:00 Download 6c05f76
Download 6c05f76 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 204 2019-11-30T10:36:10+01:00
Download abe3ea7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 204 2019-12-01T03:14:09+01:00
Download 204529a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-11T21:47:23+01:00 Download 0ea02fd
Download bf23c7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-08T00:27:29+01:00 Download 57e75e8
Download e08293b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-07T21:19:42+01:00 Download dc9f726
Download a1f2759 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-05T20:21:35+01:00 Download bf681bf
Download d336502 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-05T19:35:19+01:00 Download a81e348
Download 8a71f8c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 339 2019-11-29T14:34:05+01:00
Download 21f3880 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 339 2019-12-01T04:55:36+01:00

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

Trying to find witnesses for program (1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0, sv-benchmarks/c/eca-rers2012/Problem01_label57_false-unreach-call_false-termination.c).

Found 23 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label57_false-unreach-call_false-termination.c, 1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0a894c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T10:54 CET (sv-comp)
Download d7ec01e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 10 2018-12-08T02:56:53
Download 4b11a2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 81 2018-12-07T10:28 CET (sv-comp)
Download 1e4812f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 204 2018-12-07T14:58:52+01:00
Download 5d9caea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 206 2018-12-10T20:35:47+01:00 Download 75bb599
Download 398444d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 205 2018-12-09T18:20:08+01:00 Download f6a411d
Download 2456288 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 207 2018-12-08T23:43:55+01:00 Download 0a894c9
Download 62debae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 205 2018-12-08T22:10:47+01:00 Download d7ec01e
Download 1fe2b82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 205 2018-12-08T08:57:08+01:00 Download 1e4812f
Download bc8a159 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 205 2018-12-08T05:06:24+01:00 Download d3adeda
Download 42eca70 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 258 2018-12-07T17:45:24+01:00 Download 4b11a2d
Download a1b073e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 205 2018-12-06T10:12:01+01:00 Download 31bbf40
Download 616bdda Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 205 2018-12-06T09:48:53+01:00 Download e81c7ad
Download de5844d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 259 2018-12-06T09:09:28+01:00 Download 89dc33a
Download e81c7ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 204 2018-12-05T11:40:21+01:00
Download 463f781 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-09T20:53:26+01:00 Download 554f2e3
Download d4327f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-09T20:38:00+01:00 Download 4f47d4c
Download 1a13ac4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-09T20:34:53+01:00 Download 650e8e2
Download b6b658c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-06T09:42:39+01:00 Download 4679773
Download bd14bf8 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 339 2018-12-08T02:30:56+01:00
Download 8a370d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 336 2018-12-08T07:55:07+01:00
Download 7e08dab Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 324 2018-12-06T09:48:34+01:00
Download ce4a7c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 327 2018-12-05T06:52:17+01:00

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

Trying to find witnesses for program (1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0, sv-benchmarks/c/eca-rers2012/Problem01_label57_false-unreach-call_false-termination.c).

Found 15 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label57_false-unreach-call_false-termination.c, 1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e8a333d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Veriabs 3 2017-12-02T21:30 CET (sv-comp)
Download d4ee0b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T00:03 CET (sv-comp)
Download 4f83145 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 177 2017-12-02T10:37Z
Download 43fe359 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 5 2017-12-01T23:03:05.341554
Download 50966e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 5 2017-12-01T09:18:53.372537
Download 598df7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 15 2017-12-01T20:03 CET (sv-comp)
Download d670656 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 15 2017-12-01T04:36 CET (sv-comp)
Download c8971d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 118 2017-11-30T16:29:29+01:00
Download 7b9024d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 296 2017-11-30T14:23:06+01:00
Download 6491343 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 112 2017-11-30T12:46:02+01:00
Download af59d7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 182 2017-12-02T07:51:05+01:00
Download 72b4e1a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 89 2017-11-30T19:15 CET (sv-comp)
Download eabbadb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 177 2017-12-02T12:21Z
Download dbdb6f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 90 2017-11-30T14:45 CET (sv-comp)
Download bbbbd68 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 31 2017-12-01T12:18 CET (sv-comp)

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

Trying to find witnesses for program (1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0, sv-benchmarks/c/eca-rers2012/Problem01_label57_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label57_false-unreach-call_false-termination.c, 1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/1d9900a048ad333b785bed01fe231cb166ff4a3ffd6333a6771c6537bebaf6b0.json

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