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 29 witnesses for program sv-benchmarks/c/termination-restricted-15/PastaB14_true-termination_true-no-overflow.c, 07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8e59fc8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T06:19:00Z | ||
a83f5b8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:19:57+01:00 | ||
e0959ed | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2023-12-20T03:37 CET (comp) | ||
29ef1d9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 7 | 2023-12-02T18:00:31Z | ||
00a86c2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2023-11-29T13:12:53Z | ||
7e26fbb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 7 | 2023-12-02T23:14:52Z | ||
591bdce | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 17 | 2023-12-01T01:26:41Z | ||
4182ad4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 586 | 2023-12-20T03:55:48+01:00 | e0959ed | |
adf8413 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-19T03:33:04+01:00 | 2009630 | |
1ca0d06 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-04T11:53:32+01:00 | 29ef1d9 | |
8c9b1b9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-04T01:49:13+01:00 | e615396 | |
520197c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-03T18:46:25+01:00 | a83f5b8 | |
9d7042d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 1298 | 2023-12-03T10:01:56+01:00 | 8e59fc8 | |
cf34889 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-03T06:06:44+01:00 | 7e26fbb | |
fcdd5ef | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-01T04:05:22+01:00 | 591bdce | |
25d471c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-01T00:21:31+01:00 | 72c8975 | |
2e45b67 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9265 | 2023-11-30T12:24:41+01:00 | a6455f6 | |
a6455f6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T05:27:46+01:00 | ||
eacee6c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 870 | 2023-11-29T18:38:32+01:00 | 00a86c2 | |
0f2827e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-29T08:23:21+01:00 | 316e5b3 | |
e615396 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 5 | 2023-12-03T21:24:02+01:00 | ||
2009630 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2023-12-19T01:15:37+01:00 | ||
316e5b3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 7 | 2023-11-28T22:39:11Z | ||
72c8975 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | 2LS | 9 | 2023-11-30T23:10:19+01:00 | ||
68439f3 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 8 | 2023-11-30T22:31:58+01:00 | ||
a4ffdb2 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: e2725860-c36d-4b8b-a773-e8a3e0eddebb creation_time: '2023-12-02T19:00:32+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_30189677-7491-4167-b9f9-b3941fa05dcf/sv-benchmarks/c/termination-restricted-15/PastaB14.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_30189677-7491-4167-b9f9-b3941fa05dcf/sv-benchmarks/c/termination-restricted-15/PastaB14.c : 07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_30189677-7491-4167-b9f9-b3941fa05dcf/sv-benchmarks/c/termination-restricted-15/PastaB14.c file_hash: 07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e line: 11 column: 0 function: main value: ((((x <= 2147483647) && (0 <= (x + 2147483648))) && (0 <= (y + 2147483648))) && (y <= 2147483647)) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_30189677-7491-4167-b9f9-b3941fa05dcf/sv-benchmarks/c/termination-restricted-15/PastaB14.c file_hash: 07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e line: 12 column: 0 function: main value: (((x == y) && (0 <= y)) && (y <= 2147483647)) format: c_expression | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-04T12:18:00+01:00 | ||
6e36d7e | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 82b259ce-7166-4d48-a45e-1d37c2f5ff45 creation_time: '2023-11-28T23:39:11+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e48e2383-5485-4d48-9382-4f3612a5041d/sv-benchmarks/c/termination-restricted-15/PastaB14.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e48e2383-5485-4d48-9382-4f3612a5041d/sv-benchmarks/c/termination-restricted-15/PastaB14.c : 07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e48e2383-5485-4d48-9382-4f3612a5041d/sv-benchmarks/c/termination-restricted-15/PastaB14.c file_hash: 07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e line: 11 column: 0 function: main value: ((x <= 2147483647) && (y <= 2147483647)) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e48e2383-5485-4d48-9382-4f3612a5041d/sv-benchmarks/c/termination-restricted-15/PastaB14.c file_hash: 07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e line: 12 column: 0 function: main value: (((0 <= x) && (x <= 2147483647)) && (y <= x)) format: c_expression | correctness_witness | CPAchecker 2.3 | 281 | 2023-11-29T08:01:03+01:00 | ||
b72cded | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 5604f44b-863c-477c-bdff-b0ea536b677b creation_time: '2023-12-03T00:14:52+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0eb358d4-6dba-4a23-b65c-064ef6405033/sv-benchmarks/c/termination-restricted-15/PastaB14.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0eb358d4-6dba-4a23-b65c-064ef6405033/sv-benchmarks/c/termination-restricted-15/PastaB14.c : 07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0eb358d4-6dba-4a23-b65c-064ef6405033/sv-benchmarks/c/termination-restricted-15/PastaB14.c file_hash: 07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e line: 11 column: 0 function: main value: ((x <= 2147483647) && (y <= 2147483647)) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0eb358d4-6dba-4a23-b65c-064ef6405033/sv-benchmarks/c/termination-restricted-15/PastaB14.c file_hash: 07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e line: 12 column: 0 function: main value: ((((x < 1) && (0 <= x)) && (y < 1)) || (((x <= 2147483647) && (y <= x)) && (1 <= x))) format: c_expression | correctness_witness | CPAchecker 2.3 | 3995 | 2023-12-03T05:47:14+01:00 | ||
4a5d06c | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: bce8680f-781f-419e-871e-a492c0440b6a creation_time: 2023-12-01T01:26:41Z producer: name: Goblint version: tags/svcomp24-0-gc2e9465a7 command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--sets'' ''ana.specification'' ''../../sv-benchmarks/c/properties/no-overflow.prp'' ''--sets'' ''exp.architecture'' ''64bit'' ''../../sv-benchmarks/c/termination-restricted-15/PastaB14.c''' task: input_files: - ../../sv-benchmarks/c/termination-restricted-15/PastaB14.c input_file_hashes: ../../sv-benchmarks/c/termination-restricted-15/PastaB14.c: 07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/PastaB14.c file_hash: 07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e line: 12 column: 15 function: main value: (0LL - (long long )x) + (long long )y >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/PastaB14.c file_hash: 07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e line: 12 column: 15 function: main value: (long long )x - (long long )y >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/PastaB14.c file_hash: 07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e line: 12 column: 15 function: main value: (((((0 <= x && 0 <= y) && (long long )x + (long long )y >= 0LL) && x != -1) && y != -1) && (((x != -2 && y != -2) && (((x != -3 && y != -3) && (((x != -4 && y != -4) && (((x != -5 && y != -5) && (((x != -6 && y != -6) && (((x != -7 && y != -7) && (((x != -8 && y != -8) && (((x != -9 && y != -9) && (((x != -10 && y != -10) && (((x != -11 && y != -11) && ((((x <= 2147483635 && y <= 2147483635) && x != -12) && y != -12) || (x <= 2147483636 && y <= 2147483636))) || (x <= 2147483637 && y <= 2147483637))) || (x <= 2147483638 && y <= 2147483638))) || (x <= 2147483639 && y <= 2147483639))) || (x <= 2147483640 && y <= 2147483640))) || (x <= 2147483641 && y <= 2147483641))) || (x <= 2147483642 && y <= 2147483642))) || (x <= 2147483643 && y <= 2147483643))) || (x <= 2147483644 && y <= 2147483644))) || (x <= 2147483645 && y <= 2147483645))) || (x <= 2147483646 && y <= 2147483646))) || ((1 <= x && (-2LL + (long long )x) + (long long )y >= 0LL) && x != 0) format: c_expression | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-01T04:19:24+01:00 |
Found 24 witnesses for program sv-benchmarks/c/termination-restricted-15/PastaB14_true-termination_true-no-overflow.c, 07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
db816fb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T13:27:06Z | ||
0433f5e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-10T22:11:51+01:00 | ||
e0959ed | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2022-12-12T11:02 CET (comp) | ||
66233a6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 7 | 2022-12-14T11:11:59Z | ||
1c2b261 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2022-12-11T11:05:32Z | ||
92296ff | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 7 | 2022-12-14T21:09:10Z | ||
79d186c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp23-0-g4f5dcf38f) | 44 | 2022-12-10T03:57:35Z | ||
ec6c83d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T11:46:42+01:00 | e0959ed | |
0586e09 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T11:06:35+01:00 | 66233a6 | |
16e8990 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T07:30:44+01:00 | aa3c289 | |
c6a8707 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 2804 | 2023-01-29T06:37:48+01:00 | 92296ff | |
911adbc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 1069 | 2023-01-29T04:00:19+01:00 | 1c2b261 | |
631d32b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T03:02:41+01:00 | 7ed8173 | |
f09e328 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4553 | 2023-01-28T23:06:34+01:00 | 0433f5e | |
27fb62a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T22:43:02+01:00 | 79d186c | |
de12b43 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 12899 | 2023-01-28T18:34:23+01:00 | 006d656 | |
0b242e4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T17:47:23+01:00 | db816fb | |
dc9eb9d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 64 | 2023-01-27T23:13:09+01:00 | b77c23d | |
3c3d312 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 2751 | 2022-12-10T21:55:12+01:00 | ||
7ed8173 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 5 | 2022-12-12T00:43:17+01:00 | ||
006d656 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2022-12-10T00:44:55+01:00 | ||
aa3c289 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 7 | 2022-12-13T15:58:18Z | ||
b77c23d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | 2LS | 9 | 2022-12-08T01:29:20+01:00 | ||
2ad6f75 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 8 | 2022-12-08T00:28:10+01:00 |
Found 1 witnesses for program sv-benchmarks/c/termination-restricted-15/PastaB14_true-termination_true-no-overflow.c, 07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7f7b86b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 8 | 2021-12-05T23:24:52+01:00 |
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/PastaB14_true-termination_true-no-overflow.c, 07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/PastaB14_true-termination_true-no-overflow.c, 07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 1 witnesses for program sv-benchmarks/c/termination-restricted-15/PastaB14_true-termination_true-no-overflow.c, 07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c3c2f49 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T09:21 CET (sv-comp) |
Found 2 witnesses for program sv-benchmarks/c/termination-restricted-15/PastaB14_true-termination_true-no-overflow.c, 07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
76ea010 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 7 | 2017-12-01T18:57 CET (sv-comp) | ||
e971b25 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 8 | 2017-12-01T16:51 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/PastaB14_true-termination_true-no-overflow.c, 07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/07f4699c371f295a25887a3f67dc54332a57ae32b5b342f10fdc7ddcf36f265e.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |