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 24 witnesses for program sv-benchmarks/c/termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c, 9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2e68107 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T07:58:44Z | ||
f09cde2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:57:15+01:00 | ||
f8918ef | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2023-12-20T03:37 CET (comp) | ||
34fb784 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 9 | 2023-12-02T16:20:01Z | ||
848a796 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-20T03:41:52+01:00 | f8918ef | |
ac1ad00 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-19T14:41:56+01:00 | da8b62a | |
d928673 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-19T03:41:06+01:00 | 3b223fb | |
0e87fad | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-17T06:26:27+01:00 | 880d32b | |
27e32c8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-04T11:35:21+01:00 | 34fb784 | |
e4d5d45 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-04T01:34:47+01:00 | 865c84c | |
3e7065f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-03T18:31:03+01:00 | f09cde2 | |
f3f2e9d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-03T09:57:53+01:00 | 2e68107 | |
a1806db | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-11-30T12:13:16+01:00 | 1d1cd65 | |
1d1cd65 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-11-30T04:38:43+01:00 | ||
9e13ea1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-11-29T08:19:52+01:00 | bf7fe40 | |
865c84c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 4 | 2023-12-03T21:37:51+01:00 | ||
880d32b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2023-12-17T05:19:35+01:00 | ||
da8b62a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 4 | 2023-12-19T10:36:47+01:00 | ||
3b223fb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 4 | 2023-12-18T18:14:02+01:00 | ||
bf7fe40 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 8 | 2023-11-29T00:58:41Z | ||
23be7cd | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 3 | 2023-12-01T01:47:47Z | ||
1506b2d | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: c0b162e3-a837-43b1-9e38-22d254990ea5 creation_time: '2023-11-29T01:58:41+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f163e3af-54ac-498f-bae2-74a31c1b8635/sv-benchmarks/c/termination-crafted/Benghazi.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f163e3af-54ac-498f-bae2-74a31c1b8635/sv-benchmarks/c/termination-crafted/Benghazi.c : 9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5 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_f163e3af-54ac-498f-bae2-74a31c1b8635/sv-benchmarks/c/termination-crafted/Benghazi.c file_hash: 9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5 line: 22 column: 0 function: main value: (((((d2 == 74) && (x <= 2147483647)) && (d1 == 73)) || (((((d2 == 74) && (d1 == 75)) && (0 <= (x + 73))) && (d1 == 73)) && (x <= 2147483574))) || (((((((((((((73 <= d1) && (d2 <= 2147483647)) && (75 <= d1)) && (d1 <= 2147483645)) && (d1 <= 2147483645)) && (((d1 * 4) + (3 * x)) <= 8589934572)) && ((x + d1) <= 2147483647)) && (0 <= (x + d1))) && (x <= 2147483499)) && (1 <= (d2 + x))) && (((d2 * 4) + (3 * x)) <= 8589934576)) && (74 <= d2)) && ((d2 + x) <= 2147483648))) format: c_expression | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-29T07:48:52+01:00 | ||
fa13793 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 5f53449b-f352-41ff-a51b-54bfa00bd549 creation_time: '2023-12-02T17:20:01+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c875c161-2fd4-4012-beed-5cacfd62de71/sv-benchmarks/c/termination-crafted/Benghazi.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c875c161-2fd4-4012-beed-5cacfd62de71/sv-benchmarks/c/termination-crafted/Benghazi.c : 9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5 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_c875c161-2fd4-4012-beed-5cacfd62de71/sv-benchmarks/c/termination-crafted/Benghazi.c file_hash: 9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5 line: 22 column: 0 function: main value: (((((((((d2 == 74) && (d1 == 75)) && (0 <= (x + 73))) && (d1 == 73)) && (x <= 2147483574)) || ((((d2 == 74) && (x <= 2147483647)) && (0 <= (x + 2147483648))) && (d1 == 73))) || (((((76 == d2) && (d1 == 75)) && (0 <= (x + 75))) && (d1 == 75)) && (x <= 2147483499))) || ((((((d1 <= 2147483645) && (d1 <= 2147483645)) && ((((((d1 + x) <= 2147483570) && (75 <= d1)) && ((d1 + 1) == d2)) && (77 <= d1)) || (((((d1 + 1) == d2) && ((x + (2 * d1)) <= 2147483570)) && (79 <= d1)) && (74 <= d2)))) && (1 <= (d2 + x))) && (((d2 * 4) + (3 * x)) <= 8589934576)) && ((d2 + x) <= 2147483648))) || (((((((d2 + x) <= 2147483500) && (77 == d1)) && ((d1 + 1) == d2)) && (d2 <= 76)) && (1 <= (d2 + x))) && (74 <= d2))) format: c_expression | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-04T12:04:53+01:00 | ||
9eb6709 | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: 8295e511-5265-4e48-9e84-439e6e42371e creation_time: 2023-12-01T01:52:55Z 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-crafted/Benghazi.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted/Benghazi.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted/Benghazi.c: 9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/Benghazi.c file_hash: 9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5 line: 22 column: 8 function: main value: (((((-1LL + (long long )d2) + (long long )x >= 0LL && (-1LL - (long long )d1old) + (long long )d2 >= 0LL) && (long long )d1old + (long long )x >= 0LL) && (1LL + (long long )d1old) - (long long )d2 >= 0LL) && (((((((1LL - (long long )d1) + (long long )d2 >= 0LL && (2LL - (long long )d1) + (long long )d1old >= 0LL) && ((((((((((((((-2147483647 <= x && 79 <= d1) && 79 <= d1old) && 80 <= d2) && x <= 2147483191) && (-159LL + (long long )d1) + (long long )d2 >= 0LL) && (-159LL + (long long )d1old) + (long long )d2 >= 0LL) && (-158LL + (long long )d1) + (long long )d1old >= 0LL) && (long long )d1 + (long long )x >= 0LL) && (1LL + (long long )d1) - (long long )d2 >= 0LL) && (long long )d1 - (long long )d1old >= 0LL) && d1 % 2 == 1) && d2 % 2 == 0) && d1old % 2 == 1) || ((((((((((((((((-77 <= x && x <= 2147483270) && (-157LL + (long long )d1) + (long long )d2 >= 0LL) && (-156LL + (long long )d1) + (long long )d1old >= 0LL) && (-155LL + (long long )d1old) + (long long )d2 >= 0LL) && (-2LL + (long long )d1) + (long long )x >= 0LL) && (154LL - (long long )d1old) + (long long )x >= 0LL) && (155LL - (long long )d2) + (long long )x >= 0LL) && (156LL - (long long )d1) + (long long )x >= 0LL) && (-2LL + (long long )d1) - (long long )d1old >= 0LL) && (-1LL + (long long )d1) - (long long )d2 >= 0LL) && (155LL - (long long )d1old) - (long long )d2 >= 0LL) && (156LL - (long long )d1) - (long long )d1old >= 0LL) && (157LL - (long long )d1) - (long long )d2 >= 0LL) && d1 == 79) && d2 == 78) && d1old == 77))) || ((((((((((((((((((-77 <= x && x <= 2147483347) && (-155LL + (long long )d1) + (long long )d2 >= 0LL) && (-155LL + (long long )d1old) + (long long )d2 >= 0LL) && (-154LL + (long long )d1) + (long long )d1old >= 0LL) && (-1LL - (long long )d1) + (long long )d2 >= 0LL) && (0LL - (long long )d1) + (long long )d1old >= 0LL) && (154LL - (long long )d1) + (long long )x >= 0LL) && (154LL - (long long )d1old) + (long long )x >= 0LL) && (155LL - (long long )d2) + (long long )x >= 0LL) && (long long )d1 + (long long )x >= 0LL) && (1LL + (long long )d1) - (long long )d2 >= 0LL) && (154LL - (long long )d1) - (long long )d1old >= 0LL) && (155LL - (long long )d1) - (long long )d2 >= 0LL) && (155LL - (long long )d1old) - (long long )d2 >= 0LL) && (long long )d1 - (long long )d1old >= 0LL) && d1 == 77) && d2 == 78) && d1old == 77)) || ((((((((((((((((((-75 <= x && x <= 2147483424) && (-153LL + (long long )d1) + (long long )d2 >= 0LL) && (-152LL + (long long )d1) + (long long )d1old >= 0LL) && (-151LL + (long long )d1old) + (long long )d2 >= 0LL) && (-2LL + (long long )d1) + (long long )x >= 0LL) && (1LL - (long long )d1) + (long long )d2 >= 0LL) && (2LL - (long long )d1) + (long long )d1old >= 0LL) && (150LL - (long long )d1old) + (long long )x >= 0LL) && (151LL - (long long )d2) + (long long )x >= 0LL) && (152LL - (long long )d1) + (long long )x >= 0LL) && (-2LL + (long long )d1) - (long long )d1old >= 0LL) && (-1LL + (long long )d1) - (long long )d2 >= 0LL) && (151LL - (long long )d1old) - (long long )d2 >= 0LL) && (152LL - (long long )d1) - (long long )d1old >= 0LL) && (153LL - (long long )d1) - (long long )d2 >= 0LL) && d1 == 77) && d2 == 76) && d1old == 75)) || ((((((((((((((((((-75 <= x && x <= 2147483499) && (-151LL + (long long )d1) + (long long )d2 >= 0LL) && (-151LL + (long long )d1old) + (long long )d2 >= 0LL) && (-150LL + (long long )d1) + (long long )d1old >= 0LL) && (-1LL - (long long )d1) + (long long )d2 >= 0LL) && (0LL - (long long )d1) + (long long )d1old >= 0LL) && (150LL - (long long )d1) + (long long )x >= 0LL) && (150LL - (long long )d1old) + (long long )x >= 0LL) && (151LL - (long long )d2) + (long long )x >= 0LL) && (long long )d1 + (long long )x >= 0LL) && (1LL + (long long )d1) - (long long )d2 >= 0LL) && (150LL - (long long )d1) - (long long )d1old >= 0LL) && (151LL - (long long )d1) - (long long )d2 >= 0LL) && (151LL - (long long )d1old) - (long long )d2 >= 0LL) && (long long )d1 - (long long )d1old >= 0LL) && d1 == 75) && d2 == 76) && d1old == 75)) || (((((((((((((((((((-73 <= x && x <= 2147483574) && (-149LL + (long long )d1) + (long long )d2 >= 0LL) && (-148LL + (long long )d1) + (long long )d1old >= 0LL) && (-147LL + (long long )d1old) + (long long )d2 >= 0LL) && (-2LL + (long long )d1) + (long long )x >= 0LL) && (1LL - (long long )d1) + (long long )d2 >= 0LL) && (2LL - (long long )d1) + (long long )d1old >= 0LL) && (146LL - (long long )d1old) + (long long )x >= 0LL) && (147LL - (long long )d2) + (long long )x >= 0LL) && (148LL - (long long )d1) + (long long )x >= 0LL) && (-2LL + (long long )d1) - (long long )d1old >= 0LL) && (-1LL + (long long )d1) - (long long )d2 >= 0LL) && (147LL - (long long )d1old) - (long long )d2 >= 0LL) && (148LL - (long long )d1) - (long long )d1old >= 0LL) && (149LL - (long long )d1) - (long long )d2 >= 0LL) && 73 == d1old) && d1 == 75) && d2 == 74) && d1old == 73))) || ((((((((((((((((-147LL + (long long )d1) + (long long )d2 >= 0LL && (2147483574LL + (long long )d1old) + (long long )d2 >= 0LL) && (2147483575LL + (long long )d1) + (long long )d1old >= 0LL) && (-1LL - (long long )d1) + (long long )d2 >= 0LL) && (2147483573LL - (long long )d1old) + (long long )d2 >= 0LL) && (2147483721LL - (long long )d1) + (long long )d1old >= 0LL) && (1LL + (long long )d1) - (long long )d2 >= 0LL) && (2147483574LL + (long long )d1) - (long long )d1old >= 0LL) && (2147483722LL + (long long )d1old) - (long long )d2 >= 0LL) && (147LL - (long long )d1) - (long long )d2 >= 0LL) && (2147483720LL - (long long )d1) - (long long )d1old >= 0LL) && (2147483721LL - (long long )d1old) - (long long )d2 >= 0LL) && 73 == d1) && 74 == d2) && d1 == 73) && d2 == 74) format: c_expression | correctness_witness | CPAchecker 2.3 | 13 | 2023-12-01T03:55:46+01:00 |
Found 20 witnesses for program sv-benchmarks/c/termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c, 9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2a1db7d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T10:02:54Z | ||
69f00c1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-10T22:09:57+01:00 | ||
f8918ef | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2022-12-12T11:00 CET (comp) | ||
168af44 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 7 | 2022-12-14T08:57:46Z | ||
e78c326 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T11:32:31+01:00 | f8918ef | |
b0561f4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T10:51:44+01:00 | 168af44 | |
3ef48f2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T07:17:00+01:00 | 74e2b40 | |
b0b2ede | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T02:34:05+01:00 | 9eaa269 | |
04d91ad | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T00:06:59+01:00 | 643d4ee | |
f081c03 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T22:50:52+01:00 | 69f00c1 | |
43fc475 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T17:59:46+01:00 | 69ffd76 | |
1983e6e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T17:44:30+01:00 | 2a1db7d | |
414a09e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T11:04:51+01:00 | cfa3282 | |
6c6e9ff | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T01:01:07+01:00 | 64893e5 | |
cfa3282 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2022-12-10T20:15:39+01:00 | ||
9eaa269 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 4 | 2022-12-11T22:48:44+01:00 | ||
64893e5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2022-12-25T10:04:31+01:00 | ||
643d4ee | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 4 | 2022-12-11T04:55:47+01:00 | ||
69ffd76 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 4 | 2022-12-10T01:12:36+01:00 | ||
74e2b40 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 7 | 2022-12-13T15:08:25Z |
Found 16 witnesses for program sv-benchmarks/c/termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c, 9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
973b8e1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2021-12-06T13:43:35+01:00 | ||
2ad647f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.2.8 | 3 | 2021-12-13T21:55:58Z | ||
c53aa38 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 7 | 2021-12-10T02:45:42Z | ||
ac584e7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-14T00:10:06+01:00 | 2ad647f | |
9172426 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-10T21:01:15+01:00 | a6c0060 | |
f77ee8b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-10T08:38:29+01:00 | c53aa38 | |
c79da71 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-09T15:44:54+01:00 | 6d932e7 | |
6411e4f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-08T21:45:30+01:00 | 09cd5a9 | |
33cfb96 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-07T02:45:26+01:00 | 773357a | |
c18265d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-06T14:46:31+01:00 | 973b8e1 | |
59a3f6e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-05T20:09:40+01:00 | 3bc3afb | |
3bc3afb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-05T17:07:24+01:00 | ||
a6c0060 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 4 | 2021-12-10T17:16:37+01:00 | ||
09cd5a9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 4 | 2021-12-08T16:44:58+01:00 | ||
6d932e7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 4 | 2021-12-09T11:11:28+01:00 | ||
773357a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 7 | 2021-12-06T20:39:07Z |
Found 7 witnesses for program sv-benchmarks/c/termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c, 9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
b1cecce | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.2.1 | 3 | 2020-12-06T23:40:13 | ||
74aeeee | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | unknown_witness | Goblint (svcomp21-0-g82e03b87) | 3 | 2020-12-07T19:27:59 | ||
61e4a06 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 4 | 2020-12-09T01:58:57+01:00 | 5efe02e | |
8ae27a1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 4 | 2020-12-08T07:31:08+01:00 | 9f22a7f | |
ce4a0e5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 4 | 2020-12-06T13:13:06+01:00 | ff2b099 | |
ff2b099 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 4 | 2020-12-05T13:17:11+01:00 | ||
9f22a7f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 4 | 2020-12-08T02:29:43+01:00 |
Found 4 witnesses for program sv-benchmarks/c/termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c, 9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1af6666 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 4 | 2019-11-29T18:06:57+01:00 | ||
609af99 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 4 | 2019-12-01T03:23:25+01:00 | ||
fafe2ea | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.9 | 607 | 2019-11-29T16:43:41+01:00 | ||
8d1e82f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 607 | 2019-12-01T09:49:54+01:00 |
Found 3 witnesses for program sv-benchmarks/c/termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c, 9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
98cb22d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T00:32:49 | ||
1feaf39 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 703 | 2018-12-08T01:19:08+01:00 | ||
7b7f4fd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T07:53:40+01:00 |
Found 3 witnesses for program sv-benchmarks/c/termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c, 9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4f1b9ba | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 7 | 2017-12-03T07:44Z | ||
19b7ef5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 7 | 2017-12-03T10:33Z | ||
10ca276 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 6 | 2017-12-01T21:33 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c, 9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |