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).
Found 25 witnesses for program sv-benchmarks/c/termination-numeric/Binomial_true-termination_false-no-overflow.c, c204b56aba09d3ce87e17edffdff1d33aa0b4dc87a1e1140339548dffa982588
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/c204b56aba09d3ce87e17edffdff1d33aa0b4dc87a1e1140339548dffa982588.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
fe44faa | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T04:06:52Z | ||
e68856a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | crux-llvm-0.5.0.99 | 198 | 2023-12-18T05:17:12+01:00 | ||
0719c2e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | VeriOover | 2 | 2023-12-20T03:37 CET (comp) | ||
8651a54 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 3 | 2023-12-17T00:57:52Z | ||
16e3cda | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 3 | 2023-11-29T20:15:32Z | ||
3ab8d29 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 7.4.0 kind | 4 | 2023-12-01T12:27:35Z | ||
74db84f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CBMC | 14 | 2023-12-17T09:38:00+01:00 | ||
76b5660 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Bubaak | 3 | 2023-12-05T08:42:54Z | ||
f2d64c6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Bubaak | 3 | 2023-12-04T10:00:24Z | ||
b2fa500 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:34:43+01:00 | ||
ba54e49 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 12 | 2023-12-20T03:42:50+01:00 | 0719c2e | |
21dbd3f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 11 | 2023-12-19T04:26:25+01:00 | 48a9497 | |
7fb2fbd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 12 | 2023-12-17T06:42:36+01:00 | 8651a54 | |
4a4ba8d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 12 | 2023-12-05T14:40:15+01:00 | 76b5660 | |
c945a4b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 12 | 2023-12-04T16:41:14+01:00 | f2d64c6 | |
bf42fb8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 11 | 2023-12-04T02:04:04+01:00 | 05e3194 | |
dbf5a18 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 11 | 2023-12-03T18:47:58+01:00 | b2fa500 | |
d64f2d5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 12 | 2023-12-03T09:58:38+01:00 | fe44faa | |
5c8af45 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 13 | 2023-12-01T18:30:21+01:00 | 3ab8d29 | |
ce51052 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 11 | 2023-11-30T12:38:59+01:00 | 3712904 | |
3712904 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 11 | 2023-11-30T05:30:14+01:00 | ||
2b5943a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 12 | 2023-11-30T03:05:33+01:00 | 16e3cda | |
05e3194 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 11 | 2023-12-03T20:45:04+01:00 | ||
48a9497 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 11 | 2023-12-18T16:44:38+01:00 | ||
a751b66 | Inspect | - content: - segment: - waypoint: action: follow constraint: format: C value: \result == 13 location: column: 32 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0c5794ab-a619-424e-8a51-18995b10f901/sv-benchmarks/c/termination-numeric/Binomial.c line: 34 type: function_return - segment: - waypoint: action: follow constraint: format: C value: \result == 0 location: column: 32 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0c5794ab-a619-424e-8a51-18995b10f901/sv-benchmarks/c/termination-numeric/Binomial.c line: 37 type: function_return - segment: - waypoint: action: follow constraint: format: C value: \result == 0 location: column: 32 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0c5794ab-a619-424e-8a51-18995b10f901/sv-benchmarks/c/termination-numeric/Binomial.c line: 40 type: function_return - segment: - waypoint: action: follow location: column: 14 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0c5794ab-a619-424e-8a51-18995b10f901/sv-benchmarks/c/termination-numeric/Binomial.c line: 26 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T20:15:32Z' format_version: '0.1' producer: name: symbiotic task: data_model: LP64 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0c5794ab-a619-424e-8a51-18995b10f901/sv-benchmarks/c/termination-numeric/Binomial.c : c204b56aba09d3ce87e17edffdff1d33aa0b4dc87a1e1140339548dffa982588 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0c5794ab-a619-424e-8a51-18995b10f901/sv-benchmarks/c/termination-numeric/Binomial.c language: C specification: CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 15 | 2023-11-30T03:01:30+01:00 |
Found 22 witnesses for program sv-benchmarks/c/termination-numeric/Binomial_true-termination_false-no-overflow.c, c204b56aba09d3ce87e17edffdff1d33aa0b4dc87a1e1140339548dffa982588
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/c204b56aba09d3ce87e17edffdff1d33aa0b4dc87a1e1140339548dffa982588.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4a12172 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | verifuzz | 3 | 2022-12-15T05:59:39+01:00 | ||
018e458 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T10:36:22Z | ||
5f71695 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | crux-llvm-0.5.0.99 | 198 | 2022-12-09T03:33:12+01:00 | ||
0719c2e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | VeriOover | 2 | 2022-12-12T11:01 CET (comp) | ||
f6908f6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 3 | 2022-12-25T08:40:30Z | ||
34d07a2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 3 | 2022-12-12T13:35:48Z | ||
34c21e7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 7.0.0 kind | 4 | 2022-12-18T15:55:25Z | ||
6d51ef6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CBMC | 14 | 2022-12-08T11:15:10+01:00 | ||
4a0f249 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Bubaak | 3 | 2022-12-08T17:55:19Z | ||
cfc5cd5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-10T22:13:58+01:00 | ||
520e6e7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 12 | 2023-01-29T11:33:58+01:00 | 0719c2e | |
5077b74 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 12 | 2023-01-29T05:59:53+01:00 | 34d07a2 | |
98ed50c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 11 | 2023-01-29T02:48:52+01:00 | ee2f53d | |
691ecb0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 11 | 2023-01-28T23:07:48+01:00 | cfc5cd5 | |
ba62913 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 11 | 2023-01-28T18:27:55+01:00 | 1ff0722 | |
1560abe | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 12 | 2023-01-28T17:49:41+01:00 | 018e458 | |
8e5c705 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 13 | 2023-01-28T15:47:13+01:00 | 34c21e7 | |
be9907f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 11 | 2023-01-28T11:08:03+01:00 | f028679 | |
44c7222 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 12 | 2023-01-28T02:23:56+01:00 | f6908f6 | |
f028679 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 11 | 2022-12-10T17:43:56+01:00 | ||
ee2f53d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 11 | 2022-12-11T23:39:23+01:00 | ||
1ff0722 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 11 | 2022-12-09T23:20:42+01:00 |
Found 15 witnesses for program sv-benchmarks/c/termination-numeric/Binomial_true-termination_false-no-overflow.c, c204b56aba09d3ce87e17edffdff1d33aa0b4dc87a1e1140339548dffa982588
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/c204b56aba09d3ce87e17edffdff1d33aa0b4dc87a1e1140339548dffa982588.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8e39b7f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | verifuzz | 3 | 2021-12-11T05:03:16+01:00 | ||
f620cc3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.2.8 | 3 | 2021-12-13T21:56:51Z | ||
5d523ed | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | crux-llvm-0.5.0.99 | 198 | 2021-12-07T06:33:12+01:00 | ||
75e5ecb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 3 | 2021-12-10T16:09:02 | ||
96259d7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 3 | 2021-12-07T12:16:40Z | ||
c4de1a3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 6.8.0 kind | 4 | 2021-12-08T07:03:32Z | ||
435f61c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CBMC | 125 | 2021-12-06T09:13:00+01:00 | ||
b42ddec | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2021-12-06T14:19:55+01:00 | ||
bbd14f4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 12 | 2021-12-14T00:09:37+01:00 | f620cc3 | |
14dc2bf | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 12 | 2021-12-10T21:29:58+01:00 | 75e5ecb | |
6f649a5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 13 | 2021-12-08T13:49:59+01:00 | c4de1a3 | |
79ac20f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 12 | 2021-12-07T19:14:36+01:00 | 96259d7 | |
f3bca90 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 11 | 2021-12-05T17:33:26+01:00 | ||
e8702ac | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 11 | 2021-12-08T17:51:52+01:00 | ||
2fdbadc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 11 | 2021-12-09T12:35:06+01:00 |
Found 9 witnesses for program sv-benchmarks/c/termination-numeric/Binomial_true-termination_false-no-overflow.c, c204b56aba09d3ce87e17edffdff1d33aa0b4dc87a1e1140339548dffa982588
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/c204b56aba09d3ce87e17edffdff1d33aa0b4dc87a1e1140339548dffa982588.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6ad5edd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.2.1 | 3 | 2020-12-06T23:50:27 | ||
52ee83a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 3 | 2020-12-11T18:21:51 | ||
af5f055 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 2 | 2020-12-08T23:16:58 | ||
24eb662 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 12 | 2020-12-12T01:42:40+01:00 | 52ee83a | |
ba4537d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 12 | 2020-12-09T04:14:13+01:00 | af5f055 | |
6c45c23 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 13 | 2020-12-07T16:43:13+01:00 | eeb0c8c | |
7596d6a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 12 | 2020-12-07T00:16:30+01:00 | 6ad5edd | |
19b0dea | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 11 | 2020-12-05T15:22:41+01:00 | ||
afe72ec | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 11 | 2020-12-08T05:46:01+01:00 |
Found 6 witnesses for program sv-benchmarks/c/termination-numeric/Binomial_true-termination_false-no-overflow.c, c204b56aba09d3ce87e17edffdff1d33aa0b4dc87a1e1140339548dffa982588
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/c204b56aba09d3ce87e17edffdff1d33aa0b4dc87a1e1140339548dffa982588.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
b645eb5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 1 | 2019-12-01 02:17:00 | ||
bffe9c9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Pinaka | 114 | 2019-12-03T23:05 CET (comp) | ||
516c823 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.9 | 13 | 2019-12-11T21:10:43+01:00 | b645eb5 | |
7751851 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.9 | 13 | 2019-12-11T20:45:48+01:00 | ad44b7c | |
698904d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.9 | 12 | 2019-11-30T09:20:38+01:00 | ||
8c2e09a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 12 | 2019-12-01T02:53:36+01:00 |
Found 8 witnesses for program sv-benchmarks/c/termination-numeric/Binomial_true-termination_false-no-overflow.c, c204b56aba09d3ce87e17edffdff1d33aa0b4dc87a1e1140339548dffa982588
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/c204b56aba09d3ce87e17edffdff1d33aa0b4dc87a1e1140339548dffa982588.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
64d8763 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 2 | 2018-12-08T09:16 CET (sv-comp) | ||
1bc91b6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Pinaka | 127 | 2018-12-07T05:30 CET (sv-comp) | ||
79571de | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 13 | 2018-12-08T01:47:33+01:00 | ||
533db8f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-09T18:21:40+01:00 | cbc8d6f | |
1b96e4b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T23:44:55+01:00 | 64d8763 | |
d73b1c9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T05:06:29+01:00 | 761d15e | |
b056ca5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T02:58:08+01:00 | ||
b1f6d58 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T01:36 CET (sv-comp) |
Found 7 witnesses for program sv-benchmarks/c/termination-numeric/Binomial_true-termination_false-no-overflow.c, c204b56aba09d3ce87e17edffdff1d33aa0b4dc87a1e1140339548dffa982588
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/c204b56aba09d3ce87e17edffdff1d33aa0b4dc87a1e1140339548dffa982588.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f32f072 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 2 | 2017-12-03T04:35 CET (sv-comp) | ||
2b46944 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Map2Check | 3 | 2017-12-02T01:01 CET (sv-comp) | ||
72d83f5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T18:20:34.734551 | ||
3ea57a2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-02T05:59:18.858088 | ||
acd030e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 3.1 | 64 | 2017-12-01T14:11 CET (sv-comp) | ||
35f06c4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CBMC | 208 | 2017-12-01T11:53 CET (sv-comp) | ||
9403c21 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 51 | 2017-12-01T19:53 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-numeric/Binomial_true-termination_false-no-overflow.c, c204b56aba09d3ce87e17edffdff1d33aa0b4dc87a1e1140339548dffa982588
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/c204b56aba09d3ce87e17edffdff1d33aa0b4dc87a1e1140339548dffa982588.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |