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).
Key | Value |
programName | sv-benchmarks/c/bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i |
programSHA | 1d3530f13e3baf5919140991660f03d1cc8723ead9319a3f459bfd17defddcf7 |
witnessName | results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.byte_add_false-unreach-call_true-no-overflow_true-termination.i.files/witness.graphml |
witnessSHA | 5ee1640219e51a039832f3c6e68f6163bc5bf6913bf0ac1ce53e50a01ae37693 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-02T16:26 CET (sv-comp) |
producer | Symbiotic |
program-sha256 | 1d3530f13e3baf5919140991660f03d1cc8723ead9319a3f459bfd17defddcf7 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_cd432ca2-34f9-416f-b113-fa3bc8546c6e/sv-benchmarks/c/bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i |
programhash | a2c46755d0cb80f6b2e7b990e0a1bd9a49737b84 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/5ee1640219e51a039832f3c6e68f6163bc5bf6913bf0ac1ce53e50a01ae37693.graphml |
witness-sha256 | 5ee1640219e51a039832f3c6e68f6163bc5bf6913bf0ac1ce53e50a01ae37693 |
witness-size | 1695 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i, 1d3530f13e3baf5919140991660f03d1cc8723ead9319a3f459bfd17defddcf7
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/1d3530f13e3baf5919140991660f03d1cc8723ead9319a3f459bfd17defddcf7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i, 1d3530f13e3baf5919140991660f03d1cc8723ead9319a3f459bfd17defddcf7
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/1d3530f13e3baf5919140991660f03d1cc8723ead9319a3f459bfd17defddcf7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i, 1d3530f13e3baf5919140991660f03d1cc8723ead9319a3f459bfd17defddcf7
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/1d3530f13e3baf5919140991660f03d1cc8723ead9319a3f459bfd17defddcf7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i, 1d3530f13e3baf5919140991660f03d1cc8723ead9319a3f459bfd17defddcf7
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/1d3530f13e3baf5919140991660f03d1cc8723ead9319a3f459bfd17defddcf7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 20 witnesses for program sv-benchmarks/c/bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i, 1d3530f13e3baf5919140991660f03d1cc8723ead9319a3f459bfd17defddcf7
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/1d3530f13e3baf5919140991660f03d1cc8723ead9319a3f459bfd17defddcf7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
052e82b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2019-12-04T01:01 CET (comp) | ||
a335ede | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.9 | 19 | 2019-11-30T02:45:05+01:00 | ||
b02568b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 19 | 2019-12-01T18:59:26+01:00 | ||
b37e92b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-02 01:12:49 | ||
e590432 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 26 | 2019-12-03T21:44 CET (comp) | ||
0ac38ff | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 44 | 2019-12-11T21:52:30+01:00 | 55225cf | |
21d0553 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 58 | 2019-12-11T21:09:33+01:00 | b37e92b | |
a84170b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 43 | 2019-12-11T20:55:28+01:00 | 98e0b6e | |
ad63b43 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 57 | 2019-12-11T20:44:44+01:00 | ab4d1e8 | |
453cb31 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 43 | 2019-12-08T01:51:20+01:00 | 32e5684 | |
8564b2c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 42 | 2019-12-08T00:26:03+01:00 | f241a5f | |
c192ebe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 42 | 2019-12-07T21:13:26+01:00 | 07e9b96 | |
56d2a4d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 58 | 2019-12-04T02:58:04+01:00 | e590432 | |
4413821 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 43 | 2019-12-03T08:10:32+01:00 | f434e6c | |
f434e6c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 44 | 2019-11-30T02:23:20+01:00 | ||
32e5684 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 44 | 2019-12-07T22:24:51+01:00 | ||
55225cf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 44 | 2019-12-01T01:34:19+01:00 | ||
6098ee9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 20 | 2019-12-05T20:20:28+01:00 | 261b572 | |
ce045ef | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 20 | 2019-12-05T19:34:11+01:00 | b9cf0b9 | |
adb769c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:06 CET (comp) |
Found 29 witnesses for program sv-benchmarks/c/bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i, 1d3530f13e3baf5919140991660f03d1cc8723ead9319a3f459bfd17defddcf7
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/1d3530f13e3baf5919140991660f03d1cc8723ead9319a3f459bfd17defddcf7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
906a526 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T07:30 CET (sv-comp) | ||
1273a32 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T08:52:06 | ||
1bcc27e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2018-12-07T01:42 CET (sv-comp) | ||
1ede750 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 19 | 2018-12-08T01:54:02+01:00 | ||
733e9b5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 19 | 2018-12-06T05:14:56+01:00 | ||
139799a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 2 | 2018-12-08T03:46 CET (sv-comp) | ||
db643fb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 10 | 2018-12-08T13:18:32 | ||
d119243 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 26 | 2018-12-07T14:29 CET (sv-comp) | ||
796cb2e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 40 | 2018-12-10T17:22:28+01:00 | ||
2cf4c0e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 44 | 2018-12-07T03:32:47+01:00 | ||
27acb9b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 43 | 2018-12-10T20:35:56+01:00 | 796cb2e | |
d8dc758 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 56 | 2018-12-09T20:17:47+01:00 | 32241df | |
34a45df | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 52 | 2018-12-09T18:21:58+01:00 | 5ccc405 | |
07d5bae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 59 | 2018-12-08T23:43:14+01:00 | 139799a | |
b444065 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 49 | 2018-12-08T22:10:36+01:00 | db643fb | |
411c059 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 44 | 2018-12-08T08:47:10+01:00 | 2cf4c0e | |
fcf90eb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 46 | 2018-12-08T05:03:46+01:00 | 04c7b2d | |
388d1da | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 42 | 2018-12-07T17:44:23+01:00 | d119243 | |
f3357f0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 46 | 2018-12-06T10:13:06+01:00 | bfcba6b | |
60e79f2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 43 | 2018-12-06T09:48:00+01:00 | 9746354 | |
f7b18af | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 64 | 2018-12-06T09:12:16+01:00 | cd9fc87 | |
9746354 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 44 | 2018-12-05T18:41:14+01:00 | ||
5b3ac6d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-09T20:53:14+01:00 | e6dccd2 | |
5d5a2c7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-09T20:38:42+01:00 | 412ddb4 | |
b68272b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-07T01:16:14+01:00 | 8f389ff | |
3b3838f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-06T09:41:22+01:00 | 6b267a7 | |
358c416 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-06T09:12:04+01:00 | 6ba8189 | |
483c625 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T05:05 CET (sv-comp) | ||
667738e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T03:08 CET (sv-comp) |
Found 28 witnesses for program sv-benchmarks/c/bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i, 1d3530f13e3baf5919140991660f03d1cc8723ead9319a3f459bfd17defddcf7
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/1d3530f13e3baf5919140991660f03d1cc8723ead9319a3f459bfd17defddcf7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4d64cde | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 39 | 2017-12-03T07:44Z | ||
ec29753 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 1 | 2017-12-03T04:41 CET (sv-comp) | ||
c4def7f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Map2Check | 11 | 2017-12-02T01:16 CET (sv-comp) | ||
e083370 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 40 | 2017-12-03T10:28Z | ||
b732aad | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T17:34:38.448713 | ||
9653853 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | ESBMC 4.6.0 incr | 3 | 2017-12-02T05:37:21.134464 | ||
dfde222 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | ESBMC 3.1 | 24 | 2017-12-01T13:13 CET (sv-comp) | ||
7e25b4f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 19 | 2017-12-01T10:58:46+01:00 | ||
be7c30b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CBMC | 75 | 2017-12-01T12:12 CET (sv-comp) | ||
7670652 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 39 | 2017-12-03T10:35Z | ||
d435fff | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | 2LS | 43 | 2017-12-01T10:32 CET (sv-comp) | ||
99b1f9a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 39 | 2017-12-02T16:31Z | ||
5ee1640 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 2 | 2017-12-02T16:26 CET (sv-comp) | ||
911dbfa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Map2Check | 3 | 2017-12-01T21:32 CET (sv-comp) | ||
5ad8e03 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 47 | 2017-12-02T02:59Z | ||
886035d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 8 | 2017-12-01T14:43:34.830267 | ||
3f70076 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 8 | 2017-12-01T08:28:11.072415 | ||
f459e0e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 12 | 2017-12-01T19:44 CET (sv-comp) | ||
56f6511 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 12 | 2017-12-01T00:15 CET (sv-comp) | ||
371b836 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn | 39 | 2017-12-02T19:03:46+01:00 | ||
2a3da53 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 40 | 2017-11-30T22:49:10+01:00 | ||
d2abcc8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 31 | 2017-12-01T20:35:38+01:00 | ||
23d75b2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 32 | 2017-12-01T03:37 CET (sv-comp) | ||
969f997 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 39 | 2017-12-02T07:17Z | ||
3932dbd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 23 | 2017-11-30T22:57 CET (sv-comp) | ||
80d27f4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T23:22:43.961892 | ||
723a911 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T15:15:51.182474 | ||
a98a0ec | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 68 | 2017-12-01T15:13 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i, 1d3530f13e3baf5919140991660f03d1cc8723ead9319a3f459bfd17defddcf7
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/1d3530f13e3baf5919140991660f03d1cc8723ead9319a3f459bfd17defddcf7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |