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/loops/trex01_false-unreach-call_true-termination.i
programSHA 71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a
witnessName results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.trex01_false-unreach-call_true-termination.i.files/witness.graphml
witnessSHA 23854834dce19d3680746066b31d00daab4d937469d0ecdd3438582a8dcc223e

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-01T03:05 CET (sv-comp)
producer 2LS
program-sha256 71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a
programfile ../../sv-benchmarks/c/loops/trex01_false-unreach-call_true-termination.i
programhash b3a658a1fe592322f5aa7f1391ad7ef7d0545b11
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/23854834dce19d3680746066b31d00daab4d937469d0ecdd3438582a8dcc223e.graphml
witness-sha256 23854834dce19d3680746066b31d00daab4d937469d0ecdd3438582a8dcc223e
witness-size 5250
witness-type violation_witness

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

Trying to find witnesses for program (71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a, sv-benchmarks/c/loops/trex01_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/trex01_false-unreach-call_true-termination.i, 71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a.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 (71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a, sv-benchmarks/c/loops/trex01_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/trex01_false-unreach-call_true-termination.i, 71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a.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 (71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a, sv-benchmarks/c/loops/trex01_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/trex01_false-unreach-call_true-termination.i, 71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a.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 (71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a, sv-benchmarks/c/loops/trex01_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/trex01_false-unreach-call_true-termination.i, 71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a.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 (71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a, sv-benchmarks/c/loops/trex01_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/trex01_false-unreach-call_true-termination.i, 71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a.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 '19

Trying to find witnesses for program (71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a, sv-benchmarks/c/loops/trex01_false-unreach-call_true-termination.i).

Found 24 witnesses for program sv-benchmarks/c/loops/trex01_false-unreach-call_true-termination.i, 71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 93738ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T06:46 CET (sv-comp)
Download 9c27d55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T09:20:00
Download 3d5b5f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 5 2018-12-07T01:06 CET (sv-comp)
Download 8c2927b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 7 2018-12-10T18:08:54+01:00
Download ea12015 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 7 2018-12-07T21:38:13+01:00
Download 5ee70c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-10T20:38:16+01:00 Download 8c2927b
Download 6d1ef95 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T20:53:10+01:00 Download cf47c86
Download 1c85e2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T20:37:14+01:00 Download bedd06c
Download 18e965c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T20:34:34+01:00 Download 8b7df27
Download 50e3629 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T18:21:28+01:00 Download 3cbde99
Download f4c9629 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T23:43:52+01:00 Download 93738ad
Download bef4e35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T22:10:26+01:00 Download 9c27d55
Download 9ba3b82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T08:19:13+01:00 Download ea12015
Download 317620e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-08T05:05:10+01:00 Download ca41e46
Download 4153295 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-07T18:48:14+01:00 Download e32cb0e
Download 258f87d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-07T17:45:23+01:00 Download 3d5b5f1
Download 96b5fce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T10:17:40+01:00 Download b6dc274
Download fe174fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:48:07+01:00 Download 71b2aae
Download c2e2663 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:41:45+01:00 Download b131172
Download c92889a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:17:37+01:00 Download 7a0cdd5
Download f94a3da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:00:13+01:00 Download c644cbb
Download 71b2aae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-05T10:11:34+01:00
Download d4a67ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-08T04:36:12+01:00 Download 4a59aec
Download 7e53135 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 10 2018-12-07T01:11:31+01:00 Download bb464ed

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

Trying to find witnesses for program (71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a, sv-benchmarks/c/loops/trex01_false-unreach-call_true-termination.i).

Found 16 witnesses for program sv-benchmarks/c/loops/trex01_false-unreach-call_true-termination.i, 71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d5d95e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 4 2017-12-01T22:24 CET (sv-comp)
Download 869cb8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 6 2017-12-03T02:28Z
Download 697ccfe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T06:03 CET (sv-comp)
Download c2e919a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 6 2017-12-02T15:46Z
Download 9715102 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T23:04:43.589747
Download 3cf300f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T10:50:33.308216
Download 4d74d21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-12-01T20:12 CET (sv-comp)
Download 18622c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-12-01T00:16 CET (sv-comp)
Download a41eeb5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 7 2017-12-03T03:05:04+01:00
Download 5f5c5d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-11-30T18:22:41+01:00
Download 9d83f51 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 11 2017-11-30T13:40:24+01:00
Download 2d53978 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 6 2017-11-30T18:47:57+01:00
Download 4f08f1b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 7 2017-12-02T02:11:52+01:00
Download 360832d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 6 2017-11-30T22:06 CET (sv-comp)
Download a1b87c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 6 2017-12-02T14:30Z
Download 2385483 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 5 2017-12-01T03:05 CET (sv-comp)

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

Trying to find witnesses for program (71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a, sv-benchmarks/c/loops/trex01_false-unreach-call_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/loops/trex01_false-unreach-call_true-termination.i, 71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/71dcd0c05d8bb78a898285a8c73691612c8c31f98e96ad89660af2a0bbfbd34a.json

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