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_1_true-unreach-call_true-no-overflow_true-termination.i
programSHA 9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944
witnessName results-verified/uautomizer.2017-12-03_1117.logfiles/sv-comp18.byte_add_1_true-unreach-call_true-no-overflow_true-termination.i.files/witness.graphml
witnessSHA ac2c3045c022dab8e89f1a1c48e65ea7357dad770d97f4d05fa20faad2cb4cea

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2017-12-03T10:28Z
producer Automizer
program-sha256 9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944
programfile /tmp/vcloud-vcloud-master/worker/working_dir_25655ead-3782-4559-8d3a-3f7b1d8db05b/sv-benchmarks/c/bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i
programhash 6e973c5cecb5d30af2cf4ea74d1b0b1563334ffe
sourcecodelang C
specification CHECK( init(main()), LTL(G ! overflow) )
witness-file witnessFileByHash/ac2c3045c022dab8e89f1a1c48e65ea7357dad770d97f4d05fa20faad2cb4cea.graphml
witness-sha256 ac2c3045c022dab8e89f1a1c48e65ea7357dad770d97f4d05fa20faad2cb4cea
witness-size 39185
witness-type correctness_witness

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

Trying to find witnesses for program (9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944, sv-benchmarks/c/bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i).

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 969123c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2019-12-03T23:11 CET (comp)
Download 0540a3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 20 2019-11-30T08:16:24+01:00
Download 79ed83a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 20 2019-12-01T02:10:15+01:00
Download d7038cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2019-12-04T00:58 CET (comp)
Download bd2c167 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 19 2019-12-11T20:28:26+01:00 Download 10ef2ac
Download 83fb5bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 19 2019-12-11T20:13:00+01:00 Download b5af3a2
Download 904b552 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 19 2019-12-11T20:03:14+01:00 Download 5a1b2cd
Download 0b158e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 19 2019-12-08T00:36:29+01:00 Download 6937e86
Download 41e17c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 19 2019-12-06T02:11:14+01:00 Download 7dc6c71
Download 7d08813 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 19 2019-12-05T19:13:38+01:00 Download 4a579fc
Download e5b382b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 19 2019-12-05T19:03:08+01:00 Download b5479fd
Download 130f0da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 19 2019-12-04T02:08:03+01:00 Download d7038cb
Download fea97eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 19 2019-11-30T19:51:21+01:00 Download 13d25ba
Download dea236a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 19 2019-11-30T17:05:31+01:00 Download 963977d
Download 963977d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / svcomp20 19 2019-11-30T00:21:51+01:00
Download 6937e86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8 27 2019-12-07T13:26:13+01:00
Download b5af3a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 19 2019-12-01T00:27:22+01:00
Download 61f746b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T22:56 CET (comp)

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

Trying to find witnesses for program (9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944, sv-benchmarks/c/bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i).

Found 26 witnesses for program sv-benchmarks/c/bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i, 9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 084600f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2018-12-08T03:17 CET (sv-comp)
Download a8f4c2e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness SMACK 1.9.3 3 2018-12-07T20:56:38
Download bcdc1ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2018-12-06T22:50 CET (sv-comp)
Download d38e9fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 20 2018-12-07T02:50:13+01:00
Download 0d8a7f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-05T21:10:24+01:00
Download 7bc6982 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2018-12-08T12:39 CET (sv-comp)
Download 2716e54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness SMACK 1.9.3 3 2018-12-08T09:04:03
Download 6004aad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Pinaka 3 2018-12-07T03:29 CET (sv-comp)
Download 35d0674 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7 27 2018-12-10T17:30:12+01:00
Download 4ade45a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 24 2018-12-07T08:59:42+01:00
Download e464b03 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 26 2018-12-10T20:10:38+01:00 Download 35d0674
Download 7000a32 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-09T19:48:32+01:00 Download fadc9be
Download 932cb89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-08T23:10:03+01:00 Download 7bc6982
Download 273db25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-08T21:37:14+01:00 Download 2716e54
Download e86a9e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-08T05:09:56+01:00 Download 4ade45a
Download 0941e52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-08T04:19:37+01:00 Download c5d77c0
Download 3e0c8f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-08T02:09:05+01:00 Download 9b506e9
Download 56383df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-07T16:38:56+01:00 Download 6004aad
Download 807c1ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-06T09:28:57+01:00 Download c0e4952
Download a0e4a62 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-06T09:08:57+01:00 Download 7c1d37a
Download f78c86f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-06T08:29:43+01:00 Download 24ae525
Download b7d3583 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-06T07:58:49+01:00 Download 8c6d9ee
Download 0e16686 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 20 2018-12-06T07:12:16+01:00 Download d5ad1bc
Download 7c1d37a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 19 2018-12-05T16:53:59+01:00
Download a5848cb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T11:37 CET (sv-comp)
Download bd7b113 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T06:10 CET (sv-comp)

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

Trying to find witnesses for program (9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944, sv-benchmarks/c/bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i).

Found 36 witnesses for program sv-benchmarks/c/bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i, 9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 91d1d66 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 39 2017-12-03T07:44Z
Download be535ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2017-12-03T04:12 CET (sv-comp)
Download f2aafa6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Map2Check 9 2017-12-02T01:30 CET (sv-comp)
Download 00b6993 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 40 2017-12-03T10:38Z
Download abe8ad6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T18:17:39.299294
Download 5d04cde Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-02T06:09:45.209463
Download 45fcf91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 3.1 23 2017-12-01T13:16 CET (sv-comp)
Download a550afb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-01T11:46:11+01:00
Download 9b4e5d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 69 2017-12-01T11:38 CET (sv-comp)
Download ac2c304 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 39 2017-12-03T10:28Z
Download 3767297 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 43 2017-12-01T10:43 CET (sv-comp)
Download 7c58ff5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 31 2017-12-01T22:36:00+01:00
Download a6f7901 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Symbiotic 1 2017-12-02T04:03 CET (sv-comp)
Download a8d1f16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Map2Check 9 2017-12-01T20:50 CET (sv-comp)
Download e86f5b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness Kojak 172 2017-12-02T06:39Z
Download 60264a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T02:05:05.412020
Download 97d3b22 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T14:00:35.168512
Download 2a625b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-01T21:06:49.918966
Download af20299 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T10:41:34.803928
Download 1d5b9ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 28 2017-12-01T21:23 CET (sv-comp)
Download d36396d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 22 2017-12-03T01:01:01+01:00
Download 9a9f418 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 4 2017-12-01T04:18:44+01:00
Download d87a2f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 23 2017-12-03T04:26:41+01:00 6caa401
Download 67544f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-03T02:21:52+01:00 1557ef8
Download 9cfdaf4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-02T20:30:39+01:00 6409e8b
Download 2194734 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-02T08:36:34+01:00 1963c46
Download 4be62dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-01T22:26:35+01:00 d24e568
Download ec5c6b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-01T22:05:02+01:00 b85a7d4
Download e3147ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-01T08:13:31+01:00 8c36319
Download dbb9064 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-01T05:46:18+01:00 58aa97f
Download b0277a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-01T05:26:59+01:00 f7153b0
Download 1e4a994 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-12-01T05:15:39+01:00 a4d8415
Download 00af9de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.6.1-svn 26773 19 2017-11-30T15:45:40+01:00
Download b0c9b36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CBMC 63 2017-12-01T01:54 CET (sv-comp)
Download 361c468 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness 2LS 121 2017-11-30T12:36 CET (sv-comp)
Download e843eda Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 63 2017-12-01T15:28 CET (sv-comp)

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

Trying to find witnesses for program (9534af200f13816f4bbb1218022ee782061159f6f882fcb7a0fc9ce8ef190944, sv-benchmarks/c/bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i).

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

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