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/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i
programSHA 50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded
witnessName results-verified/cbmc.2018-12-04_2248.logfiles/sv-comp19_prop-termination.byte_add_2_true-unreach-call_true-no-overflow_true-termination.i.files/witness.graphml
witnessSHA e19ee660517122f3ad0e19984c25d8846bf14f5dc2ca08e0d6cc0b6ee787cc3e

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/e19ee660517122f3ad0e19984c25d8846bf14f5dc2ca08e0d6cc0b6ee787cc3e.json

Key Value
architecture 32bit
creationtime 2018-12-05T09:31 CET (sv-comp)
producer CBMC
programfile ../../sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i
programhash 889a23428ce9b0e3800ffce916f37e53fe302b49
sourcecodelang C
specification CHECK( init(main()), LTL(F end) )
witness-file witnessFileByHash/e19ee660517122f3ad0e19984c25d8846bf14f5dc2ca08e0d6cc0b6ee787cc3e.graphml
witness-sha256 e19ee660517122f3ad0e19984c25d8846bf14f5dc2ca08e0d6cc0b6ee787cc3e
witness-size 62638
witness-type correctness_witness

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

Trying to find witnesses for program (50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded, sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i, 50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded.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 (50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded, sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i, 50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded.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 (50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded, sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i, 50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded.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 (50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded, sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i, 50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded.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 (50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded, sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i).

Found 18 witnesses for program sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i, 50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download feefa4c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2019-12-04T01:15 CET (comp)
Download 9d6f92a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 19 2019-11-29T21:58:51+01:00
Download 25e0127 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 19 2019-12-01T16:39:16+01:00
Download ae8f47c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T01:29 CET (comp)
Download 9f5be4c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 19 2019-12-11T20:17:24+01:00 Download a5b36e1
Download 1eb4f39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 19 2019-12-11T20:12:23+01:00 Download 7104cf2
Download a3516ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 19 2019-12-11T20:02:31+01:00 Download 2ed7ff1
Download dbd300c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 19 2019-12-08T00:50:18+01:00 Download 2db3b0e
Download 39bbc8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 19 2019-12-06T02:18:32+01:00 Download e2dcef8
Download b62e807 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 19 2019-12-05T19:13:05+01:00 Download dd2ead7
Download e5b08d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 19 2019-12-05T19:02:53+01:00 Download 8c261d4
Download 0b0b86d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 19 2019-12-04T02:08:00+01:00 Download ae8f47c
Download ffefcc9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 19 2019-11-30T19:57:48+01:00 Download a25723e
Download 3ecc7e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 19 2019-11-30T16:54:39+01:00 Download 0f3f55c
Download 0f3f55c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 19 2019-11-30T10:48:48+01:00
Download 2db3b0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 27 2019-12-07T21:49:28+01:00
Download a5b36e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 19 2019-12-01T17:48:11+01:00
Download 09e6b4a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:06 CET (comp)

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

Trying to find witnesses for program (50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded, sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i).

Found 25 witnesses for program sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i, 50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download bcca920 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2018-12-08T09:32 CET (sv-comp)
Download 2b827b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness SMACK 1.9.3 3 2018-12-08T11:03:46
Download 9049fbe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2018-12-07T01:01 CET (sv-comp)
Download 4e8019f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 19 2018-12-08T04:03:36+01:00
Download 574f083 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 19 2018-12-05T12:29:54+01:00
Download af78ca1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T01:12 CET (sv-comp)
Download 26b717f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T10:51:56
Download 8f46e84 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T06:55 CET (sv-comp)
Download 3455ba3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 27 2018-12-10T17:06:12+01:00
Download 0b5b508 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 27 2018-12-06T21:20:59+01:00
Download b8e6860 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 26 2018-12-10T20:09:01+01:00 Download 3455ba3
Download e0dbee7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-08T23:08:25+01:00 Download af78ca1
Download 05fb405 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-08T21:33:32+01:00 Download 26b717f
Download 3e334f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 25 2018-12-08T06:49:14+01:00 Download 0b5b508
Download 3726776 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-08T03:21:16+01:00 Download 14abb00
Download c305d90 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-08T03:02:23+01:00 Download 23dd3ce
Download a909dab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-07T16:38:25+01:00 Download 8f46e84
Download d5b610c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-06T09:28:24+01:00 Download 8533456
Download 9a854fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-06T08:45:57+01:00 Download 7062387
Download 5a48aec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-06T08:28:51+01:00 Download 3f6044c
Download 4edbd3d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-06T08:09:50+01:00 Download 882dddc
Download 7062387 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 19 2018-12-06T07:28:58+01:00
Download 2c340c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-06T07:04:41+01:00 Download ee0b3dd
Download 8970312 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T10:23 CET (sv-comp)
Download df0d427 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T11:15 CET (sv-comp)

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

Trying to find witnesses for program (50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded, sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i).

Found 34 witnesses for program sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i, 50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8f6ec85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 39 2017-12-03T07:43Z
Download 6c13dab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2017-12-03T04:46 CET (sv-comp)
Download c88a5cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Map2Check 9 2017-12-02T01:20 CET (sv-comp)
Download a427007 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 40 2017-12-03T10:20Z
Download eabec73 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T18:29:16.072787
Download da8a60d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-02T06:53:32.459426
Download 0f1358f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 3.1 23 2017-12-01T14:09 CET (sv-comp)
Download fffa5b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-01T11:32:42+01:00
Download cffd005 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 69 2017-12-01T12:00 CET (sv-comp)
Download 24a05a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 39 2017-12-03T10:20Z
Download dcc265e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 43 2017-12-01T10:54 CET (sv-comp)
Download fa1c472 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 31 2017-12-02T06:55:43+01:00
Download 6d4c7c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-01T22:58 CET (sv-comp)
Download 2de0d08 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 9 2017-12-01T19:55 CET (sv-comp)
Download 00e2e71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T02:19:25.722328
Download c108a64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T12:25:56.294463
Download 3b4cc0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T18:03:04.967687
Download 2ea1adc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T08:34:45.188833
Download 8bf9d7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 28 2017-12-01T16:58 CET (sv-comp)
Download 6cae503 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 22 2017-12-02T22:17:19+01:00
Download be59d9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-11-30T17:17:56+01:00
Download b95f667 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 23 2017-12-03T04:06:13+01:00 3f6015c
Download d96129b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-02T20:34:17+01:00 9b70bbf
Download 88bb77d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-02T07:38:26+01:00 f69be3d
Download 4bebae0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-01T22:31:15+01:00 0e35b5b
Download 0945bae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-01T22:15:16+01:00 9d171ab
Download 13b573a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-01T08:13:04+01:00 ef38cfa
Download 9782737 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-01T06:40:10+01:00 7958a1a
Download 8f91086 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-01T04:59:30+01:00 7d54775
Download 429b91d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-01T04:49:07+01:00 e56ee3b
Download 1049f27 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-11-30T18:43:45+01:00
Download 62c42cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 63 2017-11-30T20:10 CET (sv-comp)
Download 5d1c5de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 121 2017-11-30T20:26 CET (sv-comp)
Download 0da4658 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 63 2017-12-01T16:38 CET (sv-comp)

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

Trying to find witnesses for program (50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded, sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i).

Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i, 50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/50916bc95b5eb2e84cb050fcc335a0b4bd0a28a81b090fd76978dad0498a1ded.json

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