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/implicitunsignedconversion_false-unreach-call_true-termination.c
programSHA e95689a8b9c07109c1f6aa77e8cd9c3c9f6e13517a57b1039e9d63d7d6faffe9
witnessName results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.implicitunsignedconversion_false-unreach-call_true-termination.c.files/witness.graphml
witnessSHA 31501eeb42346dde23a704ad427ac0926a32ee6b5aa8633e455b040f17acf6c3

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-01T22:12:21.497579
producer ESBMC 4.6.0 kind
program-sha256 e95689a8b9c07109c1f6aa77e8cd9c3c9f6e13517a57b1039e9d63d7d6faffe9
programfile ../../sv-benchmarks/c/bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c
programhash 59cfeb3705edf7a8f1fb3969f0cbe1c9b0cfc4af
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/31501eeb42346dde23a704ad427ac0926a32ee6b5aa8633e455b040f17acf6c3.graphml
witness-sha256 31501eeb42346dde23a704ad427ac0926a32ee6b5aa8633e455b040f17acf6c3
witness-size 3637
witness-type violation_witness

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

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

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f594eea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2019-12-01 10:38:35
Download 9ef470e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 4 2019-12-04T00:42 CET (comp)
Download cd74327 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T22:00:53+01:00 Download 333cbf6
Download f55f143 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T21:44:16+01:00 Download 117df91
Download 8731152 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T21:09:02+01:00 Download f594eea
Download ffac6c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-11T20:54:47+01:00 Download 43c32e3
Download a97dedd 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 65d9bfb
Download c0ce597 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T01:51:30+01:00 Download 50af6b5
Download 52867fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-08T00:27:03+01:00 Download b0c55d4
Download 093ca2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-07T21:16:13+01:00 Download c864b50
Download 43c9858 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-06T02:38:55+01:00 Download 3e3bd0d
Download d3e7fae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-05T20:20:40+01:00 Download 3fb0b07
Download b9cbc51 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-04T02:58:17+01:00 Download 9ef470e
Download 54d1268 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-03T08:57:46+01:00 Download 9b5d78c
Download a6907c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 5 2019-12-03T08:09:56+01:00 Download 82f5273
Download 82f5273 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 4 2019-11-30T09:54:19+01:00
Download 50af6b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 4 2019-12-07T22:26:36+01:00
Download 333cbf6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 4 2019-12-01T04:15:37+01:00
Download c4d3178 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 4 2019-12-05T19:34:29+01:00 Download ad4d076
Download c251da2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:59 CET (comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f025e76 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T08:47 CET (sv-comp)
Download ab0aecd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 3 2018-12-08T04:57:20
Download 558a7a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 4 2018-12-06T22:42 CET (sv-comp)
Download c17f580 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7 4 2018-12-10T17:31:00+01:00
Download fd3452b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-07T10:09:23+01:00
Download 69afd57 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-10T20:37:09+01:00 Download c17f580
Download 385176b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-10T10:48:50+01:00 Download 11afae2
Download c88981b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:53:21+01:00 Download 2641dda
Download 0762fd0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:35:19+01:00 Download 1a54b64
Download abda882 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:25:20+01:00 Download f20cb21
Download 1d7d4b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T18:21:49+01:00 Download 6cb88ca
Download 55094ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T23:41:57+01:00 Download f025e76
Download eb86df0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T22:09:27+01:00 Download ab0aecd
Download b5fe4d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T08:46:09+01:00 Download fd3452b
Download ed373cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T05:04:01+01:00 Download 6b74356
Download 543e93d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T03:29:24+01:00 Download 11afae2
Download 8da1313 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T18:25:34+01:00 Download 6cf3db4
Download a7d2c9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T17:44:25+01:00 Download 558a7a2
Download 1a378ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T01:20:26+01:00 Download 5fdca40
Download f015b7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T10:18:50+01:00 Download 75736e3
Download ff834e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:49:03+01:00 Download bbf5b4c
Download 19c4395 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:16:55+01:00 Download dd85edf
Download 6197c9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:11:34+01:00 Download e7ea1cd
Download bbf5b4c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-06T01:39:56+01:00
Download 03d6947 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:40:42+01:00 Download 04e7e6b
Download 71cb00c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T01:52 CET (sv-comp)
Download 48a0a2b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-06T20:27 CET (sv-comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download aa89e7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness skink 3 2017-12-01T22:47 CET (sv-comp)
Download 0aec07d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 4 2017-12-03T02:47Z
Download 7a1db1f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T12:50 CET (sv-comp)
Download 0968286 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Map2Check 3 2017-12-01T19:54 CET (sv-comp)
Download 12cc81f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 4 2017-12-02T07:25Z
Download 31501ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-01T22:12:21.497579
Download bffdec6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-01T08:20:05.386265
Download 2633acf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-12-01T15:52 CET (sv-comp)
Download c3e2fcc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 4 2017-12-01T00:36 CET (sv-comp)
Download 74e3c31 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 4 2017-12-02T18:19:59+01:00
Download eb4b7e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 4 2017-11-30T22:23:55+01:00
Download 43a5a75 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 4 2017-11-30T16:00 CET (sv-comp)
Download a99a627 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 4 2017-12-02T06:18Z
Download 04e7e6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 4 2017-11-30T15:26 CET (sv-comp)
Download 274a93a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T19:57:40.228739
Download 192e72b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T10:15:05.798273
Download 42dc982 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26758M 6 2017-12-01T02:39:17+01:00
Download 3e9c193 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26725 4 2017-11-30T14:54:57+01:00
Download b4491d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker (unknown version) 4 2017-12-02T01:20:49+01:00
Download df4dfee Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 4 2017-12-01T14:21 CET (sv-comp)
Download c6305ce Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 7 2017-12-01T13:27 CET (sv-comp)

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

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

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

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