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