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 (c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6, sv-benchmarks/c/termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c).

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
Download 233e76d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T07:44:54Z
Download f5ecc1f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:36:24+01:00
Download bb72945 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:38 CET (comp)
Download 892d451 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 15 2023-12-02T19:00:25Z
Download 9cc14ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T13:50:41Z
Download ab1d8c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-12-20T03:41:12+01:00 Download bb72945
Download c26a01e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-12-19T04:51:35+01:00 Download 009e179
Download 758f1de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-12-17T06:24:11+01:00 Download 5d8346a
Download 4dcb12d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-12-04T11:26:03+01:00 Download 892d451
Download b2f3719 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-12-04T01:50:33+01:00 Download 466ab84
Download 30ad623 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-12-03T18:34:58+01:00 Download f5ecc1f
Download 134d0ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-12-03T09:58:39+01:00 Download 233e76d
Download e49642c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-12-01T00:13:34+01:00 Download f90a862
Download aea25ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-11-30T13:07:47+01:00 Download 0c9f1cc
Download 0c9f1cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-30T07:22:12+01:00
Download 33e04f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-11-29T18:11:07+01:00 Download 9cc14ef
Download 0c277cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-11-29T08:23:23+01:00 Download 0e2e3af
Download 466ab84 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 9 2023-12-04T00:14:53+01:00
Download 5d8346a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 9 2023-12-17T04:35:20+01:00
Download 009e179 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 9 2023-12-19T01:15:17+01:00
Download 0e2e3af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 15 2023-11-29T03:58:46Z
Download f90a862 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 19 2023-11-30T22:38:27+01:00
Download a52c4e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 15 2023-11-30T22:36:53+01:00
Download e7b2112 Inspect Inspect
Validate
- 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
Download 5804c16 Inspect Inspect
Validate
- 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
Download 0aad72b Inspect Inspect
Validate
- 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

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

Trying to find witnesses for program (c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6, sv-benchmarks/c/termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c).

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
Download 74a2ad2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T13:23:50Z
Download 9152915 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Bubaak 3 2022-12-08T16:19:31Z
Download 071a88b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-11T01:47:10+01:00
Download bb72945 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T11:00 CET (comp)
Download 6287d4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 14 2022-12-14T08:26:26Z
Download 9d6d486 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T09:10:04Z
Download e34b127 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-29T11:32:12+01:00 Download bb72945
Download c43cd36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-29T10:51:26+01:00 Download 6287d4e
Download 2f71738 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-29T07:39:09+01:00 Download 2239bec
Download 1013fa6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-29T03:45:49+01:00 Download 9d6d486
Download f7bcb4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-29T03:02:55+01:00 Download cefe6cd
Download bd53d84 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-28T22:53:35+01:00 Download 071a88b
Download 1c14a8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-28T18:09:04+01:00 Download f49237e
Download c4cdc31 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-28T17:46:39+01:00 Download 74a2ad2
Download afa4a7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-28T11:22:22+01:00 Download 6f17f89
Download 1d91071 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-28T01:04:02+01:00 Download 427b06c
Download b7b8b74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-28T00:27:56+01:00 Download 9152915
Download ad6f34a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-27T23:06:15+01:00 Download 47ad663
Download 6f17f89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2022-12-10T18:18:02+01:00
Download cefe6cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 9 2022-12-12T01:03:07+01:00
Download 427b06c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 9 2022-12-25T11:41:37+01:00
Download f49237e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 9 2022-12-09T17:25:33+01:00
Download 2239bec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 14 2022-12-13T21:04:27Z
Download 47ad663 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 19 2022-12-07T23:05:40+01:00
Download f8ddc16 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 15 2022-12-07T21:21:44+01:00

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

Trying to find witnesses for program (c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6, sv-benchmarks/c/termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c).

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
Download 9b21923 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 15 2021-12-05T23:29:27+01:00

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

Trying to find witnesses for program (c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6, sv-benchmarks/c/termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c).

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

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

Trying to find witnesses for program (c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6, sv-benchmarks/c/termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c).

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
Download bace642 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.9 9 2019-11-30T11:52:34+01:00
Download ee039ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 9 2019-11-30T21:02:44+01:00

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

Trying to find witnesses for program (c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6, sv-benchmarks/c/termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c).

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

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

Trying to find witnesses for program (c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6, sv-benchmarks/c/termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c).

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
Download 7298d37 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 7 2017-12-01T21:01 CET (sv-comp)

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

Trying to find witnesses for program (c295749df38dacfa531a14c4d744c010a8ad50fab674c3b8e19c2ca945c321a6, sv-benchmarks/c/termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c).

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