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 26 witnesses for program sv-benchmarks/c/termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c, c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
233e76d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T07:44:54Z | ||
f5ecc1f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:36:24+01:00 | ||
bb72945 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2023-12-20T03:38 CET (comp) | ||
892d451 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 15 | 2023-12-02T19:00:25Z | ||
9cc14ef | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2023-11-29T13:50:41Z | ||
ab1d8c8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-20T03:41:12+01:00 | bb72945 | |
c26a01e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-19T04:51:35+01:00 | 009e179 | |
758f1de | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-17T06:24:11+01:00 | 5d8346a | |
4dcb12d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-04T11:26:03+01:00 | 892d451 | |
b2f3719 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-04T01:50:33+01:00 | 466ab84 | |
30ad623 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-03T18:34:58+01:00 | f5ecc1f | |
134d0ae | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-03T09:58:39+01:00 | 233e76d | |
e49642c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-01T00:13:34+01:00 | f90a862 | |
aea25ef | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-11-30T13:07:47+01:00 | 0c9f1cc | |
0c9f1cc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-30T07:22:12+01:00 | ||
33e04f3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-11-29T18:11:07+01:00 | 9cc14ef | |
0c277cc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-11-29T08:23:23+01:00 | 0e2e3af | |
466ab84 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 9 | 2023-12-04T00:14:53+01:00 | ||
5d8346a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 9 | 2023-12-17T04:35:20+01:00 | ||
009e179 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 9 | 2023-12-19T01:15:17+01:00 | ||
0e2e3af | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 15 | 2023-11-29T03:58:46Z | ||
f90a862 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | 2LS | 19 | 2023-11-30T22:38:27+01:00 | ||
a52c4e0 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 15 | 2023-11-30T22:36:53+01:00 | ||
e7b2112 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: c9ee2ae8-2806-4741-b8e9-db4d72ca062a creation_time: '2023-12-02T20:00:25+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4a49240c-e119-4a09-892a-0dbdd5256e70/sv-benchmarks/c/termination-crafted/Gothenburg_v2-1.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4a49240c-e119-4a09-892a-0dbdd5256e70/sv-benchmarks/c/termination-crafted/Gothenburg_v2-1.c : c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6 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_4a49240c-e119-4a09-892a-0dbdd5256e70/sv-benchmarks/c/termination-crafted/Gothenburg_v2-1.c file_hash: c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6 line: 24 column: 0 function: main value: (((((((a <= 268435455) && (a == (b + 1))) && (0 <= (268435455 + y))) && (0 <= (268435455 + b))) && ((x + 1) <= 0)) && (0 <= (268435455 + x))) && (y <= 268435455)) format: c_expression | correctness_witness | CPAchecker 2.3 | 10 | 2023-12-04T12:03:52+01:00 | ||
5804c16 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 4c3061d1-78b2-42a6-a6a2-88a02ef61c47 creation_time: '2023-11-29T04:58:46+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c41da381-6687-4cff-b934-778e8f97b685/sv-benchmarks/c/termination-crafted/Gothenburg_v2-1.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c41da381-6687-4cff-b934-778e8f97b685/sv-benchmarks/c/termination-crafted/Gothenburg_v2-1.c : c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6 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_c41da381-6687-4cff-b934-778e8f97b685/sv-benchmarks/c/termination-crafted/Gothenburg_v2-1.c file_hash: c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6 line: 24 column: 0 function: main value: (((((((0 <= ((b + y) + 2147483648)) && (a <= 268435455)) && (a == (b + 1))) && (0 <= (268435455 + b))) && ((x + 1) <= 0)) && (0 <= (268435455 + x))) && (y <= 268435455)) format: c_expression | correctness_witness | CPAchecker 2.3 | 10 | 2023-11-29T07:47:40+01:00 | ||
0aad72b | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: 1a9d6060-ad77-43e7-811d-f183419fb30d creation_time: 2023-12-01T01:33:36Z 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/Gothenburg_v2-1.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted/Gothenburg_v2-1.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted/Gothenburg_v2-1.c: c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6 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/Gothenburg_v2-1.c file_hash: c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6 line: 24 column: 12 function: main value: -268435455 <= b format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/Gothenburg_v2-1.c file_hash: c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6 line: 24 column: 12 function: main value: -268435454 <= a format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/Gothenburg_v2-1.c file_hash: c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6 line: 24 column: 12 function: main value: a <= 268435455 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/Gothenburg_v2-1.c file_hash: c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6 line: 24 column: 12 function: main value: b <= 268435454 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/Gothenburg_v2-1.c file_hash: c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6 line: 24 column: 12 function: main value: (536870909LL + (long long )a) + (long long )b >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/Gothenburg_v2-1.c file_hash: c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6 line: 24 column: 12 function: main value: (1LL - (long long )a) + (long long )b >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/Gothenburg_v2-1.c file_hash: c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6 line: 24 column: 12 function: main value: (-1LL + (long long )a) - (long long )b >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/Gothenburg_v2-1.c file_hash: c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6 line: 24 column: 12 function: main value: (536870909LL - (long long )a) - (long long )b >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/Gothenburg_v2-1.c file_hash: c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6 line: 24 column: 12 function: main value: ((((((((((((((((((((((y <= 2147483646 && (((((((((((((((((2415919108LL + (long long )a) + (long long )y >= 0LL && (2415919109LL + (long long )b) + (long long )y >= 0LL) && (2684354545LL + (long long )a) + (long long )x >= 0LL) && (2684354546LL + (long long )b) + (long long )x >= 0LL) && (3489660911LL + (long long )x) + (long long )y >= 0LL) && (2415919108LL - (long long )b) + (long long )y >= 0LL) && (2415919109LL - (long long )a) + (long long )y >= 0LL) && (2684354545LL - (long long )b) + (long long )x >= 0LL) && (2684354546LL - (long long )a) + (long long )x >= 0LL) && (2684354527LL + (long long )a) - (long long )y >= 0LL) && (2684354528LL + (long long )b) - (long long )y >= 0LL) && (5368709073LL + (long long )x) - (long long )y >= 0LL) && (2684354527LL - (long long )b) - (long long )y >= 0LL) && (2684354528LL - (long long )a) - (long long )y >= 0LL) && ((((((x <= -1 && (268435453LL + (long long )a) - (long long )x >= 0LL) && (268435454LL + (long long )b) - (long long )x >= 0LL) && (268435453LL - (long long )b) - (long long )x >= 0LL) && (268435454LL - (long long )a) - (long long )x >= 0LL) && x != 0) || ((((((x <= 2147483646 && (4831838198LL - (long long )x) + (long long )y >= 0LL) && (2415919089LL + (long long )a) - (long long )x >= 0LL) && (2415919090LL + (long long )b) - (long long )x >= 0LL) && (2415919089LL - (long long )b) - (long long )x >= 0LL) && (2415919090LL - (long long )a) - (long long )x >= 0LL) && (5100273617LL - (long long )x) - (long long )y >= 0LL))) || ((((((((x <= -1 && (2147483651LL - (long long )x) + (long long )y >= 0LL) && (268435453LL + (long long )a) - (long long )x >= 0LL) && (268435454LL + (long long )b) - (long long )x >= 0LL) && (4831838166LL + (long long )x) - (long long )y >= 0LL) && (268435453LL - (long long )b) - (long long )x >= 0LL) && (268435454LL - (long long )a) - (long long )x >= 0LL) && (2415919074LL - (long long )x) - (long long )y >= 0LL) && x != 0)) || (((x <= 2147483635 && (4294967287LL - (long long )x) + (long long )y >= 0LL) && (4831838166LL + (long long )x) - (long long )y >= 0LL) && (4563402710LL - (long long )x) - (long long )y >= 0LL))) || ((((((((((((((((((((((-2147483636 <= x && -1879048195 <= y) && x <= -1) && y <= 2147483622) && (1879048195LL + (long long )a) + (long long )y >= 0LL) && (1879048196LL + (long long )b) + (long long )y >= 0LL) && (2147483636LL + (long long )a) + (long long )x >= 0LL) && (2147483637LL + (long long )b) + (long long )x >= 0LL) && (2952790002LL + (long long )x) + (long long )y >= 0LL) && (1879048195LL - (long long )b) + (long long )y >= 0LL) && (1879048196LL - (long long )a) + (long long )y >= 0LL) && (2147483636LL - (long long )b) + (long long )x >= 0LL) && (2147483637LL - (long long )a) + (long long )x >= 0LL) && (268435453LL + (long long )a) - (long long )x >= 0LL) && (268435454LL + (long long )b) - (long long )x >= 0LL) && (2147483622LL + (long long )a) - (long long )y >= 0LL) && (2147483623LL + (long long )b) - (long long )y >= 0LL) && (4294967259LL + (long long )x) - (long long )y >= 0LL) && (268435453LL - (long long )b) - (long long )x >= 0LL) && (268435454LL - (long long )a) - (long long )x >= 0LL) && (2147483622LL - (long long )b) - (long long )y >= 0LL) && (2147483623LL - (long long )a) - (long long )y >= 0LL) && x != 0)) || (((((((((((((((((((((((-2147483636 <= x && -1879048195 <= y) && x <= 1879048180) && y <= 2147483622) && (1879048195LL + (long long )a) + (long long )y >= 0LL) && (1879048196LL + (long long )b) + (long long )y >= 0LL) && (2147483636LL + (long long )a) + (long long )x >= 0LL) && (2147483637LL + (long long )b) + (long long )x >= 0LL) && (2952790002LL + (long long )x) + (long long )y >= 0LL) && (1879048195LL - (long long )b) + (long long )y >= 0LL) && (1879048196LL - (long long )a) + (long long )y >= 0LL) && (2147483636LL - (long long )b) + (long long )x >= 0LL) && (2147483637LL - (long long )a) + (long long )x >= 0LL) && (3758096376LL - (long long )x) + (long long )y >= 0LL) && (1879048180LL + (long long )a) - (long long )x >= 0LL) && (1879048181LL + (long long )b) - (long long )x >= 0LL) && (2147483622LL + (long long )a) - (long long )y >= 0LL) && (2147483623LL + (long long )b) - (long long )y >= 0LL) && (4294967259LL + (long long )x) - (long long )y >= 0LL) && (1879048180LL - (long long )b) - (long long )x >= 0LL) && (1879048181LL - (long long )a) - (long long )x >= 0LL) && (2147483622LL - (long long )b) - (long long )y >= 0LL) && (2147483623LL - (long long )a) - (long long )y >= 0LL) && (4026531803LL - (long long )x) - (long long )y >= 0LL)) || (((((((((((-1879048182 <= x && -1610612739 <= y) && x <= -1) && y <= 1879048170) && (1610612738LL - (long long )x) + (long long )y >= 0LL) && (268435453LL + (long long )a) - (long long )x >= 0LL) && (268435454LL + (long long )b) - (long long )x >= 0LL) && (3758096352LL + (long long )x) - (long long )y >= 0LL) && (268435453LL - (long long )b) - (long long )x >= 0LL) && (268435454LL - (long long )a) - (long long )x >= 0LL) && (1879048169LL - (long long )x) - (long long )y >= 0LL) && x != 0)) || ((((((-1879048182 <= x && -1610612739 <= y) && x <= 1610612726) && y <= 1879048170) && (3221225465LL - (long long )x) + (long long )y >= 0LL) && (3758096352LL + (long long )x) - (long long )y >= 0LL) && (3489660896LL - (long long )x) - (long long )y >= 0LL)) || ((((((((((((((((((((((-1610612727 <= x && -1342177282 <= y) && x <= -1) && y <= 1610612717) && (1342177282LL + (long long )a) + (long long )y >= 0LL) && (1342177283LL + (long long )b) + (long long )y >= 0LL) && (1610612727LL + (long long )a) + (long long )x >= 0LL) && (1610612728LL + (long long )b) + (long long )x >= 0LL) && (2415919093LL + (long long )x) + (long long )y >= 0LL) && (1342177282LL - (long long )b) + (long long )y >= 0LL) && (1342177283LL - (long long )a) + (long long )y >= 0LL) && (1610612727LL - (long long )b) + (long long )x >= 0LL) && (1610612728LL - (long long )a) + (long long )x >= 0LL) && (268435453LL + (long long )a) - (long long )x >= 0LL) && (268435454LL + (long long )b) - (long long )x >= 0LL) && (1610612717LL + (long long )a) - (long long )y >= 0LL) && (1610612718LL + (long long )b) - (long long )y >= 0LL) && (3221225445LL + (long long )x) - (long long )y >= 0LL) && (268435453LL - (long long )b) - (long long )x >= 0LL) && (268435454LL - (long long )a) - (long long )x >= 0LL) && (1610612717LL - (long long )b) - (long long )y >= 0LL) && (1610612718LL - (long long )a) - (long long )y >= 0LL) && x != 0)) || (((((((((((((((((((((((-1610612727 <= x && -1342177282 <= y) && x <= 1342177271) && y <= 1610612717) && (1342177282LL + (long long )a) + (long long )y >= 0LL) && (1342177283LL + (long long )b) + (long long )y >= 0LL) && (1610612727LL + (long long )a) + (long long )x >= 0LL) && (1610612728LL + (long long )b) + (long long )x >= 0LL) && (2415919093LL + (long long )x) + (long long )y >= 0LL) && (1342177282LL - (long long )b) + (long long )y >= 0LL) && (1342177283LL - (long long )a) + (long long )y >= 0LL) && (1610612727LL - (long long )b) + (long long )x >= 0LL) && (1610612728LL - (long long )a) + (long long )x >= 0LL) && (2684354554LL - (long long )x) + (long long )y >= 0LL) && (1342177271LL + (long long )a) - (long long )x >= 0LL) && (1342177272LL + (long long )b) - (long long )x >= 0LL) && (1610612717LL + (long long )a) - (long long )y >= 0LL) && (1610612718LL + (long long )b) - (long long )y >= 0LL) && (3221225445LL + (long long )x) - (long long )y >= 0LL) && (1342177271LL - (long long )b) - (long long )x >= 0LL) && (1342177272LL - (long long )a) - (long long )x >= 0LL) && (1610612717LL - (long long )b) - (long long )y >= 0LL) && (1610612718LL - (long long )a) - (long long )y >= 0LL) && (2952789989LL - (long long )x) - (long long )y >= 0LL)) || (((((((((((-1342177273 <= x && -1073741826 <= y) && x <= -1) && y <= 1342177265) && (1073741825LL - (long long )x) + (long long )y >= 0LL) && (268435453LL + (long long )a) - (long long )x >= 0LL) && (268435454LL + (long long )b) - (long long )x >= 0LL) && (2684354538LL + (long long )x) - (long long )y >= 0LL) && (268435453LL - (long long )b) - (long long )x >= 0LL) && (268435454LL - (long long )a) - (long long )x >= 0LL) && (1342177264LL - (long long )x) - (long long )y >= 0LL) && x != 0)) || ((((((-1342177273 <= x && -1073741826 <= y) && x <= 1073741817) && y <= 1342177265) && (2147483643LL - (long long )x) + (long long )y >= 0LL) && (2684354538LL + (long long )x) - (long long )y >= 0LL) && (2415919082LL - (long long )x) - (long long )y >= 0LL)) || ((((((((((((((((((((((-1073741818 <= x && -805306369 <= y) && x <= -1) && y <= 1073741812) && (805306369LL + (long long )a) + (long long )y >= 0LL) && (805306370LL + (long long )b) + (long long )y >= 0LL) && (1073741818LL + (long long )a) + (long long )x >= 0LL) && (1073741819LL + (long long )b) + (long long )x >= 0LL) && (1879048184LL + (long long )x) + (long long )y >= 0LL) && (805306369LL - (long long )b) + (long long )y >= 0LL) && (805306370LL - (long long )a) + (long long )y >= 0LL) && (1073741818LL - (long long )b) + (long long )x >= 0LL) && (1073741819LL - (long long )a) + (long long )x >= 0LL) && (268435453LL + (long long )a) - (long long )x >= 0LL) && (268435454LL + (long long )b) - (long long )x >= 0LL) && (1073741812LL + (long long )a) - (long long )y >= 0LL) && (1073741813LL + (long long )b) - (long long )y >= 0LL) && (2147483631LL + (long long )x) - (long long )y >= 0LL) && (268435453LL - (long long )b) - (long long )x >= 0LL) && (268435454LL - (long long )a) - (long long )x >= 0LL) && (1073741812LL - (long long )b) - (long long )y >= 0LL) && (1073741813LL - (long long )a) - (long long )y >= 0LL) && x != 0)) || (((((((((((((((((((((((-1073741818 <= x && -805306369 <= y) && x <= 805306362) && y <= 1073741812) && (805306369LL + (long long )a) + (long long )y >= 0LL) && (805306370LL + (long long )b) + (long long )y >= 0LL) && (1073741818LL + (long long )a) + (long long )x >= 0LL) && (1073741819LL + (long long )b) + (long long )x >= 0LL) && (1879048184LL + (long long )x) + (long long )y >= 0LL) && (805306369LL - (long long )b) + (long long )y >= 0LL) && (805306370LL - (long long )a) + (long long )y >= 0LL) && (1073741818LL - (long long )b) + (long long )x >= 0LL) && (1073741819LL - (long long )a) + (long long )x >= 0LL) && (1610612732LL - (long long )x) + (long long )y >= 0LL) && (805306362LL + (long long )a) - (long long )x >= 0LL) && (805306363LL + (long long )b) - (long long )x >= 0LL) && (1073741812LL + (long long )a) - (long long )y >= 0LL) && (1073741813LL + (long long )b) - (long long )y >= 0LL) && (2147483631LL + (long long )x) - (long long )y >= 0LL) && (805306362LL - (long long )b) - (long long )x >= 0LL) && (805306363LL - (long long )a) - (long long )x >= 0LL) && (1073741812LL - (long long )b) - (long long )y >= 0LL) && (1073741813LL - (long long )a) - (long long )y >= 0LL) && (1879048175LL - (long long )x) - (long long )y >= 0LL)) || ((((((((((((-805306364 <= x && -536870913 <= y) && x <= -1) && y <= 805306360) && (1342177277LL + (long long )x) + (long long )y >= 0LL) && (536870912LL - (long long )x) + (long long )y >= 0LL) && (268435453LL + (long long )a) - (long long )x >= 0LL) && (268435454LL + (long long )b) - (long long )x >= 0LL) && (1610612724LL + (long long )x) - (long long )y >= 0LL) && (268435453LL - (long long )b) - (long long )x >= 0LL) && (268435454LL - (long long )a) - (long long )x >= 0LL) && (805306359LL - (long long )x) - (long long )y >= 0LL) && x != 0)) || (((((((-805306364 <= x && -536870913 <= y) && x <= 536870908) && y <= 805306360) && (1342177277LL + (long long )x) + (long long )y >= 0LL) && (1073741821LL - (long long )x) + (long long )y >= 0LL) && (1610612724LL + (long long )x) - (long long )y >= 0LL) && (1342177268LL - (long long )x) - (long long )y >= 0LL)) || ((((((((((((((((((((((-536870911 <= y && -536870909 <= x) && x <= -1) && y <= 805306362) && (268435456LL + (long long )a) + (long long )y >= 0LL) && (268435457LL + (long long )b) + (long long )y >= 0LL) && (536870909LL + (long long )a) + (long long )x >= 0LL) && (536870910LL + (long long )b) + (long long )x >= 0LL) && (805306366LL + (long long )x) + (long long )y >= 0LL) && (268435456LL - (long long )b) + (long long )y >= 0LL) && (268435457LL - (long long )a) + (long long )y >= 0LL) && (536870909LL - (long long )b) + (long long )x >= 0LL) && (536870910LL - (long long )a) + (long long )x >= 0LL) && (268435453LL + (long long )a) - (long long )x >= 0LL) && (268435454LL + (long long )b) - (long long )x >= 0LL) && (536870907LL + (long long )a) - (long long )y >= 0LL) && (536870908LL + (long long )b) - (long long )y >= 0LL) && (1073741817LL + (long long )x) - (long long )y >= 0LL) && (268435453LL - (long long )b) - (long long )x >= 0LL) && (268435454LL - (long long )a) - (long long )x >= 0LL) && (536870907LL - (long long )b) - (long long )y >= 0LL) && (536870908LL - (long long )a) - (long long )y >= 0LL) && x != 0)) || (((((((((((((((((((((((-805306364 <= x && -536870911 <= y) && x <= 536870908) && y <= 805306362) && (268435456LL + (long long )a) + (long long )y >= 0LL) && (268435457LL + (long long )b) + (long long )y >= 0LL) && (536870909LL + (long long )a) + (long long )x >= 0LL) && (536870910LL + (long long )b) + (long long )x >= 0LL) && (805306366LL + (long long )x) + (long long )y >= 0LL) && (268435456LL - (long long )b) + (long long )y >= 0LL) && (268435457LL - (long long )a) + (long long )y >= 0LL) && (536870909LL - (long long )b) + (long long )x >= 0LL) && (536870910LL - (long long )x) + (long long )y >= 0LL) && (536870910LL - (long long )a) + (long long )x >= 0LL) && (268435453LL + (long long )a) - (long long )x >= 0LL) && (268435454LL + (long long )b) - (long long )x >= 0LL) && (536870907LL + (long long )a) - (long long )y >= 0LL) && (536870908LL + (long long )b) - (long long )y >= 0LL) && (1073741817LL + (long long )x) - (long long )y >= 0LL) && (268435453LL - (long long )b) - (long long )x >= 0LL) && (268435454LL - (long long )a) - (long long )x >= 0LL) && (536870907LL - (long long )b) - (long long )y >= 0LL) && (536870908LL - (long long )a) - (long long )y >= 0LL) && (805306361LL - (long long )x) - (long long )y >= 0LL)) || ((((((x <= -1 && y <= 2147483646) && (268435453LL + (long long )a) - (long long )x >= 0LL) && (268435454LL + (long long )b) - (long long )x >= 0LL) && (268435453LL - (long long )b) - (long long )x >= 0LL) && (268435454LL - (long long )a) - (long long )x >= 0LL) && x != 0)) || (x <= 2147483646 && y <= 2147483646)) || ((((((((((((((((((((((((-268435455 <= x && -268435455 <= y) && x <= -1) && y <= 268435455) && (536870909LL + (long long )a) + (long long )x >= 0LL) && (536870909LL + (long long )a) + (long long )y >= 0LL) && (536870910LL + (long long )x) + (long long )y >= 0LL) && (536870910LL + (long long )b) + (long long )x >= 0LL) && (536870910LL + (long long )b) + (long long )y >= 0LL) && (268435454LL - (long long )x) + (long long )y >= 0LL) && (536870909LL - (long long )b) + (long long )x >= 0LL) && (536870909LL - (long long )b) + (long long )y >= 0LL) && (536870910LL - (long long )a) + (long long )x >= 0LL) && (536870910LL - (long long )a) + (long long )y >= 0LL) && (268435453LL + (long long )a) - (long long )x >= 0LL) && (268435454LL + (long long )b) - (long long )x >= 0LL) && (536870909LL + (long long )a) - (long long )y >= 0LL) && (536870910LL + (long long )x) - (long long )y >= 0LL) && (536870910LL + (long long )b) - (long long )y >= 0LL) && (268435453LL - (long long )b) - (long long )x >= 0LL) && (268435454LL - (long long )x) - (long long )y >= 0LL) && (268435454LL - (long long )a) - (long long )x >= 0LL) && (536870909LL - (long long )b) - (long long )y >= 0LL) && (536870910LL - (long long )a) - (long long )y >= 0LL) && x != 0)) || ((((((((((((((((((((((((-268435455 <= x && -268435455 <= y) && x <= -1) && y <= 268435455) && (536870909LL + (long long )a) + (long long )x >= 0LL) && (536870909LL + (long long )a) + (long long )y >= 0LL) && (536870910LL + (long long )x) + (long long )y >= 0LL) && (536870910LL + (long long )b) + (long long )x >= 0LL) && (536870910LL + (long long )b) + (long long )y >= 0LL) && (268435454LL - (long long )x) + (long long )y >= 0LL) && (536870909LL - (long long )b) + (long long )x >= 0LL) && (536870909LL - (long long )b) + (long long )y >= 0LL) && (536870910LL - (long long )a) + (long long )x >= 0LL) && (536870910LL - (long long )a) + (long long )y >= 0LL) && (268435453LL + (long long )a) - (long long )x >= 0LL) && (268435454LL + (long long )b) - (long long )x >= 0LL) && (536870909LL + (long long )a) - (long long )y >= 0LL) && (536870910LL + (long long )x) - (long long )y >= 0LL) && (536870910LL + (long long )b) - (long long )y >= 0LL) && (268435453LL - (long long )b) - (long long )x >= 0LL) && (268435454LL - (long long )x) - (long long )y >= 0LL) && (268435454LL - (long long )a) - (long long )x >= 0LL) && (536870909LL - (long long )b) - (long long )y >= 0LL) && (536870910LL - (long long )a) - (long long )y >= 0LL) && x != 0)) || ((((((((((((((((((((x <= -1 && y <= 2147483646) && (2952790021LL + (long long )a) + (long long )y >= 0LL) && (2952790022LL + (long long )b) + (long long )y >= 0LL) && (3221225454LL + (long long )a) + (long long )x >= 0LL) && (3221225455LL + (long long )b) + (long long )x >= 0LL) && (4026531820LL + (long long )x) + (long long )y >= 0LL) && (2952790021LL - (long long )b) + (long long )y >= 0LL) && (2952790022LL - (long long )a) + (long long )y >= 0LL) && (3221225454LL - (long long )b) + (long long )x >= 0LL) && (3221225455LL - (long long )a) + (long long )x >= 0LL) && (268435453LL + (long long )a) - (long long )x >= 0LL) && (268435454LL + (long long )b) - (long long )x >= 0LL) && (3221225432LL + (long long )a) - (long long )y >= 0LL) && (3221225433LL + (long long )b) - (long long )y >= 0LL) && (6442450887LL + (long long )x) - (long long )y >= 0LL) && (268435453LL - (long long )b) - (long long )x >= 0LL) && (268435454LL - (long long )a) - (long long )x >= 0LL) && (3221225432LL - (long long )b) - (long long )y >= 0LL) && (3221225433LL - (long long )a) - (long long )y >= 0LL) && x != 0)) || (((((((((((((((((((((x <= 2147483646 && y <= 2147483646) && (2952790021LL + (long long )a) + (long long )y >= 0LL) && (2952790022LL + (long long )b) + (long long )y >= 0LL) && (3221225454LL + (long long )a) + (long long )x >= 0LL) && (3221225455LL + (long long )b) + (long long )x >= 0LL) && (4026531820LL + (long long )x) + (long long )y >= 0LL) && (2952790021LL - (long long )b) + (long long )y >= 0LL) && (2952790022LL - (long long )a) + (long long )y >= 0LL) && (3221225454LL - (long long )b) + (long long )x >= 0LL) && (3221225455LL - (long long )a) + (long long )x >= 0LL) && (5905580020LL - (long long )x) + (long long )y >= 0LL) && (2952789998LL + (long long )a) - (long long )x >= 0LL) && (2952789999LL + (long long )b) - (long long )x >= 0LL) && (3221225432LL + (long long )a) - (long long )y >= 0LL) && (3221225433LL + (long long )b) - (long long )y >= 0LL) && (6442450887LL + (long long )x) - (long long )y >= 0LL) && (2952789998LL - (long long )b) - (long long )x >= 0LL) && (2952789999LL - (long long )a) - (long long )x >= 0LL) && (3221225432LL - (long long )b) - (long long )y >= 0LL) && (3221225433LL - (long long )a) - (long long )y >= 0LL) && (6174015431LL - (long long )x) - (long long )y >= 0LL)) || (((((((((x <= -1 && y <= 2147483646) && (2684354564LL - (long long )x) + (long long )y >= 0LL) && (268435453LL + (long long )a) - (long long )x >= 0LL) && (268435454LL + (long long )b) - (long long )x >= 0LL) && (5905579980LL + (long long )x) - (long long )y >= 0LL) && (268435453LL - (long long )b) - (long long )x >= 0LL) && (268435454LL - (long long )a) - (long long )x >= 0LL) && (2952789979LL - (long long )x) - (long long )y >= 0LL) && x != 0)) || ((((x <= 2147483646 && y <= 2147483646) && (5368709109LL - (long long )x) + (long long )y >= 0LL) && (5905579980LL + (long long )x) - (long long )y >= 0LL) && (5637144524LL - (long long )x) - (long long )y >= 0LL) format: c_expression | correctness_witness | CPAchecker 2.3 | 39 | 2023-12-01T05:32:21+01:00 |
Found 25 witnesses for program sv-benchmarks/c/termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c, c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
74a2ad2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T13:23:50Z | ||
9152915 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Bubaak | 3 | 2022-12-08T16:19:31Z | ||
071a88b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-11T01:47:10+01:00 | ||
bb72945 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2022-12-12T11:00 CET (comp) | ||
6287d4e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 14 | 2022-12-14T08:26:26Z | ||
9d6d486 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2022-12-11T09:10:04Z | ||
e34b127 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-29T11:32:12+01:00 | bb72945 | |
c43cd36 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-29T10:51:26+01:00 | 6287d4e | |
2f71738 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-29T07:39:09+01:00 | 2239bec | |
1013fa6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-29T03:45:49+01:00 | 9d6d486 | |
f7bcb4e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-29T03:02:55+01:00 | cefe6cd | |
bd53d84 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-28T22:53:35+01:00 | 071a88b | |
1c14a8e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-28T18:09:04+01:00 | f49237e | |
c4cdc31 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-28T17:46:39+01:00 | 74a2ad2 | |
afa4a7f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-28T11:22:22+01:00 | 6f17f89 | |
1d91071 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-28T01:04:02+01:00 | 427b06c | |
b7b8b74 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-28T00:27:56+01:00 | 9152915 | |
ad6f34a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-27T23:06:15+01:00 | 47ad663 | |
6f17f89 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2022-12-10T18:18:02+01:00 | ||
cefe6cd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 9 | 2022-12-12T01:03:07+01:00 | ||
427b06c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 9 | 2022-12-25T11:41:37+01:00 | ||
f49237e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 9 | 2022-12-09T17:25:33+01:00 | ||
2239bec | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 14 | 2022-12-13T21:04:27Z | ||
47ad663 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | 2LS | 19 | 2022-12-07T23:05:40+01:00 | ||
f8ddc16 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 15 | 2022-12-07T21:21:44+01:00 |
Found 1 witnesses for program sv-benchmarks/c/termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c, c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9b21923 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 15 | 2021-12-05T23:29:27+01:00 |
Found 0 witnesses for program sv-benchmarks/c/termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c, c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 2 witnesses for program sv-benchmarks/c/termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c, c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
bace642 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 9 | 2019-11-30T11:52:34+01:00 | ||
ee039ef | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 9 | 2019-11-30T21:02:44+01:00 |
Found 0 witnesses for program sv-benchmarks/c/termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c, c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 1 witnesses for program sv-benchmarks/c/termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c, c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7298d37 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 7 | 2017-12-01T21:01 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c, c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |