Witness Inspection

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).

This link does not point to a witness, but below is a list of witnesses for the same program.

Available Results for the Program from Witness Store SV-COMP '24

Trying to find witnesses for program (9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5, sv-benchmarks/c/termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c).

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
Download 2e68107 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T07:58:44Z
Download f09cde2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:57:15+01:00
Download f8918ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download 34fb784 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 9 2023-12-02T16:20:01Z
Download 848a796 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-20T03:41:52+01:00 Download f8918ef
Download ac1ad00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-19T14:41:56+01:00 Download da8b62a
Download d928673 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-19T03:41:06+01:00 Download 3b223fb
Download 0e87fad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-17T06:26:27+01:00 Download 880d32b
Download 27e32c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-04T11:35:21+01:00 Download 34fb784
Download e4d5d45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-04T01:34:47+01:00 Download 865c84c
Download 3e7065f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-03T18:31:03+01:00 Download f09cde2
Download f3f2e9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-03T09:57:53+01:00 Download 2e68107
Download a1806db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-30T12:13:16+01:00 Download 1d1cd65
Download 1d1cd65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-30T04:38:43+01:00
Download 9e13ea1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-29T08:19:52+01:00 Download bf7fe40
Download 865c84c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 4 2023-12-03T21:37:51+01:00
Download 880d32b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2023-12-17T05:19:35+01:00
Download da8b62a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2023-12-19T10:36:47+01:00
Download 3b223fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2023-12-18T18:14:02+01:00
Download bf7fe40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 8 2023-11-29T00:58:41Z
Download 23be7cd Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 3 2023-12-01T01:47:47Z
Download 1506b2d Inspect Inspect
Validate
- 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
Download fa13793 Inspect Inspect
Validate
- 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
Download 9eb6709 Inspect Inspect
Validate
- 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

Available Results for the Program from Witness Store SV-COMP '23

Trying to find witnesses for program (9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5, sv-benchmarks/c/termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c).

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
Download 2a1db7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T10:02:54Z
Download 69f00c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:09:57+01:00
Download f8918ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T11:00 CET (comp)
Download 168af44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 7 2022-12-14T08:57:46Z
Download e78c326 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T11:32:31+01:00 Download f8918ef
Download b0561f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T10:51:44+01:00 Download 168af44
Download 3ef48f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T07:17:00+01:00 Download 74e2b40
Download b0b2ede Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T02:34:05+01:00 Download 9eaa269
Download 04d91ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T00:06:59+01:00 Download 643d4ee
Download f081c03 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T22:50:52+01:00 Download 69f00c1
Download 43fc475 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T17:59:46+01:00 Download 69ffd76
Download 1983e6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T17:44:30+01:00 Download 2a1db7d
Download 414a09e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T11:04:51+01:00 Download cfa3282
Download 6c6e9ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T01:01:07+01:00 Download 64893e5
Download cfa3282 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2022-12-10T20:15:39+01:00
Download 9eaa269 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 4 2022-12-11T22:48:44+01:00
Download 64893e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2022-12-25T10:04:31+01:00
Download 643d4ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2022-12-11T04:55:47+01:00
Download 69ffd76 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2022-12-10T01:12:36+01:00
Download 74e2b40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 7 2022-12-13T15:08:25Z

Available Results for the Program from Witness Store SV-COMP '22

Trying to find witnesses for program (9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5, sv-benchmarks/c/termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c).

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
Download 973b8e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2021-12-06T13:43:35+01:00
Download 2ad647f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.2.8 3 2021-12-13T21:55:58Z
Download c53aa38 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 7 2021-12-10T02:45:42Z
Download ac584e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-14T00:10:06+01:00 Download 2ad647f
Download 9172426 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-10T21:01:15+01:00 Download a6c0060
Download f77ee8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-10T08:38:29+01:00 Download c53aa38
Download c79da71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-09T15:44:54+01:00 Download 6d932e7
Download 6411e4f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-08T21:45:30+01:00 Download 09cd5a9
Download 33cfb96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-07T02:45:26+01:00 Download 773357a
Download c18265d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-06T14:46:31+01:00 Download 973b8e1
Download 59a3f6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-05T20:09:40+01:00 Download 3bc3afb
Download 3bc3afb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-05T17:07:24+01:00
Download a6c0060 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2021-12-10T17:16:37+01:00
Download 09cd5a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 4 2021-12-08T16:44:58+01:00
Download 6d932e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 4 2021-12-09T11:11:28+01:00
Download 773357a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 7 2021-12-06T20:39:07Z

Available Results for the Program from Witness Store SV-COMP '21

Trying to find witnesses for program (9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5, sv-benchmarks/c/termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c).

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
Download b1cecce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.1 3 2020-12-06T23:40:13
Download 74aeeee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) unknown_witness Goblint (svcomp21-0-g82e03b87) 3 2020-12-07T19:27:59
Download 61e4a06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-09T01:58:57+01:00 Download 5efe02e
Download 8ae27a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-08T07:31:08+01:00 Download 9f22a7f
Download ce4a0e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-06T13:13:06+01:00 Download ff2b099
Download ff2b099 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-05T13:17:11+01:00
Download 9f22a7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 4 2020-12-08T02:29:43+01:00

Available Results for the Program from Witness Store SV-COMP '20

Trying to find witnesses for program (9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5, sv-benchmarks/c/termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c).

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
Download 1af6666 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 4 2019-11-29T18:06:57+01:00
Download 609af99 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 4 2019-12-01T03:23:25+01:00
Download fafe2ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 607 2019-11-29T16:43:41+01:00
Download 8d1e82f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 607 2019-12-01T09:49:54+01:00

Available Results for the Program from Witness Store SV-COMP '19

Trying to find witnesses for program (9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5, sv-benchmarks/c/termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c).

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
Download 98cb22d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness SMACK 1.9.3 3 2018-12-08T00:32:49
Download 1feaf39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 703 2018-12-08T01:19:08+01:00
Download 7b7f4fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T07:53:40+01:00

Available Results for the Program from Witness Store SV-COMP '18

Trying to find witnesses for program (9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5, sv-benchmarks/c/termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c).

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
Download 4f1b9ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 7 2017-12-03T07:44Z
Download 19b7ef5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 7 2017-12-03T10:33Z
Download 10ca276 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 6 2017-12-01T21:33 CET (sv-comp)

Available Results for the Program from Witness Store SV-COMP '17

Trying to find witnesses for program (9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5, sv-benchmarks/c/termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c).

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