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/bitvector-regression/signextension_false-unreach-call_true-termination.c
programSHA 8d39710a9759cda6c47269dfa9f5bb850b936147cc5de34a7016f5d4f8b049c5
witnessName results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.signextension_false-unreach-call_true-termination.c.files/witness.graphml
witnessSHA e4476d5d6ed576daec4a07100533f340a548f2852ee6e9155be51d316681c30d

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-01T02:30:19+01:00
producer CPAchecker 1.6.1-svn 26725
program-sha256 8d39710a9759cda6c47269dfa9f5bb850b936147cc5de34a7016f5d4f8b049c5
programfile ../../sv-benchmarks/c/bitvector-regression/signextension_false-unreach-call_true-termination.c
programhash 93417fec817c517a78d8232b303da21d88847972
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/e4476d5d6ed576daec4a07100533f340a548f2852ee6e9155be51d316681c30d.graphml
witness-sha256 e4476d5d6ed576daec4a07100533f340a548f2852ee6e9155be51d316681c30d
witness-size 4301
witness-type correctness_witness

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

Trying to find witnesses for program (8d39710a9759cda6c47269dfa9f5bb850b936147cc5de34a7016f5d4f8b049c5, sv-benchmarks/c/bitvector-regression/signextension_false-unreach-call_true-termination.c).

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

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

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

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

Found 20 witnesses for program sv-benchmarks/c/bitvector-regression/signextension_false-unreach-call_true-termination.c, 8d39710a9759cda6c47269dfa9f5bb850b936147cc5de34a7016f5d4f8b049c5
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/8d39710a9759cda6c47269dfa9f5bb850b936147cc5de34a7016f5d4f8b049c5.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e6ed219 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 21:04:18
Download a5826db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 5 2019-12-03T23:19 CET (comp)
Download af884c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T22:00:21+01:00 Download 0d6f9d7
Download e20cf0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T21:40:37+01:00 Download b41a5e5
Download 2925e9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 7 2019-12-11T21:09:31+01:00 Download e6ed219
Download 80b7fea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-11T20:54:19+01:00 Download 27a5548
Download 46b2509 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 7 2019-12-11T20:44:26+01:00 Download f335d36
Download 39adbb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T01:51:13+01:00 Download c35d00f
Download 3033601 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-08T00:26:46+01:00 Download 6bc9483
Download 2d3ac5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-07T21:18:15+01:00 Download 85f7edc
Download cacdde9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-06T02:38:18+01:00 Download 97fc573
Download bb7bc59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-05T20:20:12+01:00 Download 79a0cb0
Download 0398b18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-04T02:58:14+01:00 Download a5826db
Download 3159c93 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-03T08:57:20+01:00 Download 5b85cb9
Download 3e28cd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6 2019-12-03T08:09:53+01:00 Download e9eea25
Download e9eea25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 6 2019-11-30T06:37:37+01:00
Download c35d00f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 5 2019-12-07T10:56:49+01:00
Download b41a5e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 6 2019-12-01T10:04:17+01:00
Download 033fff3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:34:16+01:00 Download 674a5b4
Download fb47380 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T01:06 CET (comp)

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

Trying to find witnesses for program (8d39710a9759cda6c47269dfa9f5bb850b936147cc5de34a7016f5d4f8b049c5, sv-benchmarks/c/bitvector-regression/signextension_false-unreach-call_true-termination.c).

Found 27 witnesses for program sv-benchmarks/c/bitvector-regression/signextension_false-unreach-call_true-termination.c, 8d39710a9759cda6c47269dfa9f5bb850b936147cc5de34a7016f5d4f8b049c5
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/8d39710a9759cda6c47269dfa9f5bb850b936147cc5de34a7016f5d4f8b049c5.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 85018a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T12:03 CET (sv-comp)
Download 26516ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 4 2018-12-08T00:44:06
Download d1a137b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 6 2018-12-07T12:26 CET (sv-comp)
Download 050e628 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 5 2018-12-10T17:19:38+01:00
Download 4aac121 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 6 2018-12-06T13:01:12+01:00
Download 1c1ed73 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-10T20:35:01+01:00 Download 050e628
Download 13cc455 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-10T10:48:44+01:00 Download f1c5026
Download e79bf77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:53:08+01:00 Download 4fe4c8f
Download 80f1f14 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:37:36+01:00 Download da4a32f
Download b9ac9dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T20:35:19+01:00 Download 4f8b013
Download 47147f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 7 2018-12-09T18:07:44+01:00 Download f6a9620
Download d9321a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T23:44:31+01:00 Download 85018a9
Download b4766f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T22:10:06+01:00 Download 26516ac
Download c33cdcf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T07:52:59+01:00 Download 4aac121
Download 66a665b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T05:04:34+01:00 Download 867cb4d
Download bdd69e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-08T03:35:47+01:00 Download f1c5026
Download 891c138 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-07T18:46:54+01:00 Download cc4f808
Download 445ae26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-07T17:44:53+01:00 Download d1a137b
Download 93a2e7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-07T01:20:51+01:00 Download 9a11b55
Download f489cc2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T10:19:00+01:00 Download e1b857f
Download 290a749 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:48:07+01:00 Download 36774aa
Download 3593b89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:10:11+01:00 Download 26bca16
Download 901094b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:00:20+01:00 Download 7f60814
Download 36774aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T07:16:03+01:00
Download b5102ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:40:41+01:00 Download 0911771
Download edb9327 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T17:19 CET (sv-comp)
Download d6c231b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T11:02 CET (sv-comp)

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

Trying to find witnesses for program (8d39710a9759cda6c47269dfa9f5bb850b936147cc5de34a7016f5d4f8b049c5, sv-benchmarks/c/bitvector-regression/signextension_false-unreach-call_true-termination.c).

Found 21 witnesses for program sv-benchmarks/c/bitvector-regression/signextension_false-unreach-call_true-termination.c, 8d39710a9759cda6c47269dfa9f5bb850b936147cc5de34a7016f5d4f8b049c5
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/8d39710a9759cda6c47269dfa9f5bb850b936147cc5de34a7016f5d4f8b049c5.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f93ab06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T22:35 CET (sv-comp)
Download 5cf1812 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 6 2017-12-02T17:29Z
Download b911a01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T07:23 CET (sv-comp)
Download cb5a5e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 4 2017-12-01T19:51 CET (sv-comp)
Download d68e850 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 6 2017-12-02T11:42Z
Download fcc695e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T14:33:33.674616
Download 3560109 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T15:17:07.452537
Download d085cff 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 dff4d69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 5 2017-12-01T06:46 CET (sv-comp)
Download 1079b47 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 5 2017-12-02T21:04:42+01:00
Download cecb2b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-11-30T22:28:56+01:00
Download 2ff9d7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 6 2017-11-30T17:02 CET (sv-comp)
Download 2ca20cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 6 2017-12-02T21:39Z
Download 0911771 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 6 2017-11-30T15:13 CET (sv-comp)
Download 8db76ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T00:30:46.957639
Download f1469b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T10:14:36.905924
Download ebc16e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 10 2017-11-30T19:43:17+01:00
Download e4476d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 4 2017-12-01T02:30:19+01:00
Download f69c288 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 4 2017-12-01T22:32:29+01:00
Download 4ce3a27 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 5 2017-12-01T18:22 CET (sv-comp)
Download 01f44a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 11 2017-12-01T16:15 CET (sv-comp)

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

Trying to find witnesses for program (8d39710a9759cda6c47269dfa9f5bb850b936147cc5de34a7016f5d4f8b049c5, sv-benchmarks/c/bitvector-regression/signextension_false-unreach-call_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/bitvector-regression/signextension_false-unreach-call_true-termination.c, 8d39710a9759cda6c47269dfa9f5bb850b936147cc5de34a7016f5d4f8b049c5
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/8d39710a9759cda6c47269dfa9f5bb850b936147cc5de34a7016f5d4f8b049c5.json

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