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 27 witnesses for program sv-benchmarks/c/termination-restricted-15/b.11_true-termination_true-no-overflow.c, 5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
08be215 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T06:54:41Z | ||
f615d42 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:42:29+01:00 | ||
2650acd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2023-12-20T03:37 CET (comp) | ||
1f135cd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 16 | 2023-12-02T13:36:21Z | ||
fd624d0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 17 | 2023-12-02T23:03:45Z | ||
f55c911 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-20T03:41:11+01:00 | 2650acd | |
c9bccd9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-19T05:04:24+01:00 | dcc4186 | |
1f0bf61 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-17T06:07:10+01:00 | 07a90ec | |
b6c7cb7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-04T11:23:31+01:00 | 1f135cd | |
42b72cf | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-04T02:01:10+01:00 | 3efc508 | |
8aeaacc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T18:29:35+01:00 | f615d42 | |
7c7c8b6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T10:00:16+01:00 | 08be215 | |
215f561 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T05:52:46+01:00 | fd624d0 | |
c112f19 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T23:48:59+01:00 | edaa935 | |
bf68567 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T12:24:15+01:00 | e815d04 | |
e815d04 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T05:09:06+01:00 | ||
d255050 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-29T08:07:59+01:00 | 36e74a6 | |
3efc508 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 6 | 2023-12-03T23:54:41+01:00 | ||
07a90ec | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 6 | 2023-12-17T03:37:30+01:00 | ||
dcc4186 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2023-12-18T22:37:26+01:00 | ||
36e74a6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 16 | 2023-11-29T03:13:17Z | ||
edaa935 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | 2LS | 12 | 2023-11-30T22:43:12+01:00 | ||
dd4510d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 9 | 2023-11-30T09:40:09+01:00 | ||
46de296 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: abce676f-e5fe-4400-a709-57d2d3911eb3 creation_time: '2023-12-03T00:03:45+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_1da5eaa1-1d3b-4bcb-9d58-79e0c160e5c2/sv-benchmarks/c/termination-restricted-15/b.11.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_1da5eaa1-1d3b-4bcb-9d58-79e0c160e5c2/sv-benchmarks/c/termination-restricted-15/b.11.c : 5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d 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_1da5eaa1-1d3b-4bcb-9d58-79e0c160e5c2/sv-benchmarks/c/termination-restricted-15/b.11.c file_hash: 5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d line: 11 column: 0 function: main value: ((((((y + 2147483648) < 0) && (0 <= (x + 1))) && ((x + 1) <= 0)) || ((((x + 1) < 0) && (0 <= (x + 2147483648))) && ((y + 2147483648) < 0))) || ((((x <= 2147483647) && (0 <= (x + 2147483648))) && (0 <= (y + 2147483648))) && (y <= 2147483647))) format: c_expression | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-03T05:33:19+01:00 | ||
8249faf | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: a92486f9-a888-4f5f-ab22-b4185f7b1378 creation_time: '2023-12-02T14:36:21+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f8fb6ff1-c000-40e6-95cc-78e48c5026fa/sv-benchmarks/c/termination-restricted-15/b.11.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f8fb6ff1-c000-40e6-95cc-78e48c5026fa/sv-benchmarks/c/termination-restricted-15/b.11.c : 5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d 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_f8fb6ff1-c000-40e6-95cc-78e48c5026fa/sv-benchmarks/c/termination-restricted-15/b.11.c file_hash: 5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d line: 11 column: 0 function: main value: (((((x <= 2147483647) && (0 <= (x + 2147483648))) && (0 <= (y + 2147483648))) && (y <= 2147483647)) || (((0 <= (x + 2147483646)) && (y <= 2147483647)) && ((x + 1) <= 0))) format: c_expression | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-04T12:03:35+01:00 | ||
eecba33 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 9fb4c1ac-5f05-4796-949e-8b0a419c4656 creation_time: '2023-11-29T04:13:17+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c14e408c-160a-4ae7-9428-deb609e93fe4/sv-benchmarks/c/termination-restricted-15/b.11.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c14e408c-160a-4ae7-9428-deb609e93fe4/sv-benchmarks/c/termination-restricted-15/b.11.c : 5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d 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_c14e408c-160a-4ae7-9428-deb609e93fe4/sv-benchmarks/c/termination-restricted-15/b.11.c file_hash: 5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d line: 11 column: 0 function: main value: (((((x <= 2147483647) && (0 <= (x + 2147483648))) && (0 <= (y + 2147483648))) && (y <= 2147483647)) || (((0 <= (x + 2147483646)) && (y <= 2147483647)) && ((x + 1) <= 0))) format: c_expression | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-29T07:48:02+01:00 | ||
ef9a990 | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: 3867ea85-8331-4479-b3f8-6d8f2436bd7f creation_time: 2023-12-01T01:07:54Z 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/b.11.c''' task: input_files: - ../../sv-benchmarks/c/termination-restricted-15/b.11.c input_file_hashes: ../../sv-benchmarks/c/termination-restricted-15/b.11.c: 5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d 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/b.11.c file_hash: 5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d line: 11 column: 13 function: main value: 0 == c format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/b.11.c file_hash: 5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d line: 11 column: 13 function: main value: c == 0 format: c_expression | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-01T05:20:49+01:00 |
Found 24 witnesses for program sv-benchmarks/c/termination-restricted-15/b.11_true-termination_true-no-overflow.c, 5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7290b89 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | verifuzz | 3 | 2022-12-15T05:53:16+01:00 | ||
e29eb53 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T09:46:31Z | ||
ae66ed8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-10T22:06:21+01:00 | ||
2650acd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2022-12-12T11:00 CET (comp) | ||
15b4059 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 16 | 2022-12-14T04:18:21Z | ||
91bafc0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 16 | 2022-12-15T00:48:41Z | ||
6441311 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T11:32:15+01:00 | 2650acd | |
bb6098a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T11:00:45+01:00 | 15b4059 | |
ee433c4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T07:40:12+01:00 | 545746d | |
f710fdd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T06:23:15+01:00 | 91bafc0 | |
e1eb888 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T03:09:06+01:00 | d25ef77 | |
d726e66 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T22:51:53+01:00 | ae66ed8 | |
2faba1b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T18:28:27+01:00 | f603cc9 | |
612aee0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T17:44:18+01:00 | e29eb53 | |
735edfd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T10:53:44+01:00 | d3dcde5 | |
414312b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T00:32:29+01:00 | a7efd6b | |
e0e96a8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-27T23:12:17+01:00 | 69c3af2 | |
d3dcde5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2022-12-10T17:16:15+01:00 | ||
d25ef77 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 6 | 2022-12-12T00:29:19+01:00 | ||
a7efd6b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 6 | 2022-12-25T10:17:11+01:00 | ||
f603cc9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2022-12-09T17:17:01+01:00 | ||
545746d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 16 | 2022-12-13T13:20:54Z | ||
69c3af2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | 2LS | 12 | 2022-12-07T22:53:32+01:00 | ||
47c4444 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 9 | 2022-12-08T01:43:11+01:00 |
Found 1 witnesses for program sv-benchmarks/c/termination-restricted-15/b.11_true-termination_true-no-overflow.c, 5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
512c64f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 9 | 2021-12-05T21:09:08+01:00 |
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/b.11_true-termination_true-no-overflow.c, 5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d.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/b.11_true-termination_true-no-overflow.c, 5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d.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/b.11_true-termination_true-no-overflow.c, 5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 2 witnesses for program sv-benchmarks/c/termination-restricted-15/b.11_true-termination_true-no-overflow.c, 5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8eb4f05 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 7 | 2017-12-01T19:43 CET (sv-comp) | ||
c2a5925 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 9 | 2017-12-01T17:18 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/b.11_true-termination_true-no-overflow.c, 5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/5b4c99d0b33a566b40cf4365ddd1611945e8961cf9631a2c233f1ae25de30e8d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |