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/recursive-simple/sum_2x3_false-unreach-call_true-termination.c
programSHA dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d
witnessName results-verified/map2check.2017-12-01_1946.logfiles/sv-comp18.sum_2x3_false-unreach-call_true-termination.c.files/witness.graphml
witnessSHA 6269e911a021c64c55ab5472655e0170f4bbd69e054e1115e6658a387110e46d

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-01T21:07 CET (sv-comp)
producer Map2Check
program-sha256 dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d
programfile ../../sv-benchmarks/c/recursive-simple/sum_2x3_false-unreach-call_true-termination.c
programhash 5417ea5971c5cfa3624e07fbe8bf33ef4632cb6f
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/6269e911a021c64c55ab5472655e0170f4bbd69e054e1115e6658a387110e46d.graphml
witness-sha256 6269e911a021c64c55ab5472655e0170f4bbd69e054e1115e6658a387110e46d
witness-size 3743
witness-type violation_witness

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

Trying to find witnesses for program (dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d, sv-benchmarks/c/recursive-simple/sum_2x3_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/sum_2x3_false-unreach-call_true-termination.c, dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d.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 (dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d, sv-benchmarks/c/recursive-simple/sum_2x3_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/sum_2x3_false-unreach-call_true-termination.c, dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d.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 (dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d, sv-benchmarks/c/recursive-simple/sum_2x3_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/sum_2x3_false-unreach-call_true-termination.c, dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d.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 (dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d, sv-benchmarks/c/recursive-simple/sum_2x3_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/sum_2x3_false-unreach-call_true-termination.c, dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d.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 (dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d, sv-benchmarks/c/recursive-simple/sum_2x3_false-unreach-call_true-termination.c).

Found 18 witnesses for program sv-benchmarks/c/recursive-simple/sum_2x3_false-unreach-call_true-termination.c, dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c140f9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 02:39:41
Download 451bb88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 6 2019-12-04T01:13 CET (comp)
Download 90f9f4d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-11T21:44:00+01:00 Download b7c2b8a
Download f7d2861 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-11T21:40:47+01:00 Download 8c5ac31
Download f50326d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-11T21:09:30+01:00 Download c140f9f
Download 1b296d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-11T20:54:46+01:00 Download 96fd4fe
Download 6924a67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-11T20:44:29+01:00 Download 2ad7c8d
Download 18dabb4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-08T00:26:12+01:00 Download 72615d8
Download 1bdf981 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-07T21:18:32+01:00 Download 51bc560
Download cb6f178 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-06T02:38:02+01:00 Download 1693ed3
Download ddd0fe1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-05T20:20:56+01:00 Download 06f1bd1
Download 8439491 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-04T02:58:02+01:00 Download 451bb88
Download 7c963b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-03T08:56:56+01:00 Download c4cb376
Download cebe501 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 8 2019-12-03T08:10:28+01:00 Download 4588e6c
Download 4588e6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 8 2019-11-30T12:25:15+01:00
Download 8c5ac31 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 8 2019-12-01T17:03:19+01:00
Download b5496c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T01:52:34+01:00 Download 3982fb4
Download 1f7c11a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:47 CET (comp)

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

Trying to find witnesses for program (dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d, sv-benchmarks/c/recursive-simple/sum_2x3_false-unreach-call_true-termination.c).

Found 26 witnesses for program sv-benchmarks/c/recursive-simple/sum_2x3_false-unreach-call_true-termination.c, dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 9dfe65f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T12:15 CET (sv-comp)
Download c072a3f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T02:48:53
Download 1846e44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 6 2018-12-07T09:46 CET (sv-comp)
Download 7f5087f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 8 2018-12-06T20:19:07+01:00
Download 7162012 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-10T10:48:51+01:00 Download a7635be
Download 513b2fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T21:23:40+01:00 Download 4fb86bf
Download e75257b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T20:53:05+01:00 Download 7532e33
Download 35ee50f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T20:39:30+01:00 Download 8f63757
Download 6e5556e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T20:21:16+01:00 Download 80a5b46
Download 720080a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T18:16:55+01:00 Download 3cf7f21
Download 2263e1f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T23:44:49+01:00 Download 9dfe65f
Download 597241d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T22:11:07+01:00 Download c072a3f
Download 668ebc6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T08:09:38+01:00 Download 7f5087f
Download bbbf000 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T05:06:20+01:00 Download f9f62dc
Download b833c85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T03:39:39+01:00 Download a7635be
Download be2e2a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-07T18:47:37+01:00 Download 4416495
Download 6da34d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-07T17:43:14+01:00 Download 1846e44
Download d3b1635 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-07T01:19:25+01:00 Download 22decd9
Download f73324d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T10:18:50+01:00 Download 920a914
Download 9761a68 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:49:01+01:00 Download b219f6d
Download 609e42d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:20:20+01:00 Download bf4aa0b
Download 4c28323 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:08:57+01:00 Download 86fe74b
Download b219f6d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T01:10:21+01:00
Download 0aa92b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-10T20:37:38+01:00 Download e092a0c
Download ccc22b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T12:54 CET (sv-comp)
Download 22660e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T01:34 CET (sv-comp)

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

Trying to find witnesses for program (dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d, sv-benchmarks/c/recursive-simple/sum_2x3_false-unreach-call_true-termination.c).

Found 20 witnesses for program sv-benchmarks/c/recursive-simple/sum_2x3_false-unreach-call_true-termination.c, dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b64a3dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T22:19 CET (sv-comp)
Download e819b84 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 6 Sat Dec 2 20:01:11 2017
Download 4fb86bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VIAP 6 2017-12-03T03:46 CET (sv-comp)
Download 6873cea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 8 2017-12-02T18:07Z
Download 67ec6ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T08:50 CET (sv-comp)
Download 6269e91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 4 2017-12-01T21:07 CET (sv-comp)
Download 0afb544 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 8 2017-12-02T09:32Z
Download 1b6ed4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T02:10:24.496160
Download 4703060 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T08:52:30.858836
Download 4b72f34 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-12-01T19:01 CET (sv-comp)
Download 38c76b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-12-01T02:29 CET (sv-comp)
Download d8969b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T03:01:34+01:00
Download bb3636c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 9 2017-12-01T02:10:59+01:00
Download c14378d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 5 2017-11-30T15:39:26+01:00
Download f60cd60 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 6 2017-12-01T22:31:06+01:00
Download 0639e91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 6 2017-11-30T21:16 CET (sv-comp)
Download a5a9027 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 8 2017-12-02T18:46Z
Download ac0d0ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T00:20:20.657802
Download cfb05e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T13:33:11.264463
Download 6dc2954 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 6 2017-12-01T16:13 CET (sv-comp)

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

Trying to find witnesses for program (dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d, sv-benchmarks/c/recursive-simple/sum_2x3_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/recursive-simple/sum_2x3_false-unreach-call_true-termination.c, dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/dae50a763509306120840982ae283833e09dbe7e323af89bb694effa66d5957d.json

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