ff6e8e1 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T07:31:39Z |
|
d5a5d25 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T18:00:44+01:00 |
|
9d2fa97 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:37 CET (comp) |
|
8ba2025 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
8 |
2023-12-02T07:23:27Z |
|
31606a5 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Pinaka |
3 |
2023-12-19T19:34:36 |
|
6bbf0aa |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Mopsa (v1.0~pre2) |
3 |
2023-11-29T12:10:37Z |
|
b04e84e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Kojak |
9 |
2023-12-02T23:00:25Z |
|
2370f2a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
24 |
2023-12-01T01:12:42Z |
|
64ec8ad |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-20T03:41:25+01:00 |
9d2fa97 |
99c95cc |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-20T02:19:20+01:00 |
31606a5 |
1a23187 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-19T14:58:29+01:00 |
20596a0 |
de608fa |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-19T03:27:53+01:00 |
972bfd6 |
e294e50 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-17T06:11:23+01:00 |
45ba984 |
1cbca42 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-04T11:45:10+01:00 |
8ba2025 |
a1cc54a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-04T02:05:18+01:00 |
a135bab |
cfd7d15 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-03T18:33:24+01:00 |
d5a5d25 |
97342f9 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-03T09:59:19+01:00 |
ff6e8e1 |
59b1507 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-03T05:46:54+01:00 |
b04e84e |
4a95a34 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-01T03:46:21+01:00 |
2370f2a |
64b7af0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-11-30T23:51:27+01:00 |
8e7462f |
a6c346b |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-11-30T13:05:30+01:00 |
749100d |
749100d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-11-30T07:05:00+01:00 |
|
bda025e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-11-29T18:21:58+01:00 |
6bbf0aa |
5a9514d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-11-29T07:55:09+01:00 |
20fbf5c |
a135bab |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
6 |
2023-12-03T23:00:30+01:00 |
|
45ba984 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.1 |
6 |
2023-12-17T03:30:00+01:00 |
|
972bfd6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
6 |
2023-12-18T19:13:11+01:00 |
|
20fbf5c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
8 |
2023-11-29T04:46:58Z |
|
8e7462f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
2LS |
1757 |
2023-11-30T21:03:12+01:00 |
|
ef86434 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: e98a042a-19ef-40f6-ac0f-ba8f53659579
creation_time: '2023-12-03T00:00:25+01:00'
producer:
name: Kojak
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_96d62010-9f9e-4132-a3ea-4518a45d4af6/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_96d62010-9f9e-4132-a3ea-4518a45d4af6/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
: 9200f4b7c01ae534db411c2832d0714b6eaa58a9d668730c8aeb9497dccadca2
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_96d62010-9f9e-4132-a3ea-4518a45d4af6/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
file_hash: 9200f4b7c01ae534db411c2832d0714b6eaa58a9d668730c8aeb9497dccadca2
line: 19
column: 0
function: main
value: (x <= 1073741823)
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_96d62010-9f9e-4132-a3ea-4518a45d4af6/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
file_hash: 9200f4b7c01ae534db411c2832d0714b6eaa58a9d668730c8aeb9497dccadca2
line: 22
column: 0
function: main
value: ((((x <= 1073741823) && (0 <= x)) && (x <= y)) || (((x <= 1073741823) && (1 <= y)) && (y < x)))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-03T05:31:27+01:00 |
|
a398b5e |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 715f30a8-7498-4e5f-8726-c77ad156cfa5
creation_time: '2023-12-02T08:23:27+01:00'
producer:
name: Taipan
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_936c08e6-99db-4f54-8544-5f37acbd3f59/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_936c08e6-99db-4f54-8544-5f37acbd3f59/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
: 9200f4b7c01ae534db411c2832d0714b6eaa58a9d668730c8aeb9497dccadca2
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_936c08e6-99db-4f54-8544-5f37acbd3f59/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
file_hash: 9200f4b7c01ae534db411c2832d0714b6eaa58a9d668730c8aeb9497dccadca2
line: 19
column: 0
function: main
value: (x < 1073741824)
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_936c08e6-99db-4f54-8544-5f37acbd3f59/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
file_hash: 9200f4b7c01ae534db411c2832d0714b6eaa58a9d668730c8aeb9497dccadca2
line: 22
column: 0
function: main
value: (((x <= 1073741823) && (0 <= x)) && (1 <= y))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-04T11:59:43+01:00 |
|
47c2209 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 34d8ed7a-9c6c-4ffb-b226-e095d2819d82
creation_time: '2023-11-29T05:46:58+01:00'
producer:
name: Automizer
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ef6317c4-87a4-4384-9f70-de0c622eccf3/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ef6317c4-87a4-4384-9f70-de0c622eccf3/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
: 9200f4b7c01ae534db411c2832d0714b6eaa58a9d668730c8aeb9497dccadca2
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_ef6317c4-87a4-4384-9f70-de0c622eccf3/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
file_hash: 9200f4b7c01ae534db411c2832d0714b6eaa58a9d668730c8aeb9497dccadca2
line: 19
column: 0
function: main
value: (x < 1073741824)
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ef6317c4-87a4-4384-9f70-de0c622eccf3/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
file_hash: 9200f4b7c01ae534db411c2832d0714b6eaa58a9d668730c8aeb9497dccadca2
line: 22
column: 0
function: main
value: (((x <= 1073741823) && (0 <= x)) && (1 <= y))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-29T07:50:14+01:00 |
|
598cb50 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: 8866ad47-9acc-4451-b457-3ffdfccbebad
creation_time: 2023-12-01T01:12:42Z
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-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c'''
task:
input_files:
- ../../sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
input_file_hashes:
../../sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c: 9200f4b7c01ae534db411c2832d0714b6eaa58a9d668730c8aeb9497dccadca2
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-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
file_hash: 9200f4b7c01ae534db411c2832d0714b6eaa58a9d668730c8aeb9497dccadca2
line: 19
column: 9
function: main
value: -1 <= x
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
file_hash: 9200f4b7c01ae534db411c2832d0714b6eaa58a9d668730c8aeb9497dccadca2
line: 19
column: 9
function: main
value: x <= 1073741823
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
file_hash: 9200f4b7c01ae534db411c2832d0714b6eaa58a9d668730c8aeb9497dccadca2
line: 19
column: 9
function: main
value: (1LL + (long long )n) + (long long )x >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
file_hash: 9200f4b7c01ae534db411c2832d0714b6eaa58a9d668730c8aeb9497dccadca2
line: 19
column: 9
function: main
value: (1073741824LL - (long long )n) + (long long )x >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
file_hash: 9200f4b7c01ae534db411c2832d0714b6eaa58a9d668730c8aeb9497dccadca2
line: 19
column: 9
function: main
value: (2147483646LL - (long long )n) - (long long )x >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
file_hash: 9200f4b7c01ae534db411c2832d0714b6eaa58a9d668730c8aeb9497dccadca2
line: 19
column: 9
function: main
value: (long long )n - (long long )x >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
file_hash: 9200f4b7c01ae534db411c2832d0714b6eaa58a9d668730c8aeb9497dccadca2
line: 22
column: 11
function: main
value: x <= 1073741823
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
file_hash: 9200f4b7c01ae534db411c2832d0714b6eaa58a9d668730c8aeb9497dccadca2
line: 22
column: 11
function: main
value: (2147483646LL - (long long )n) - (long long )x >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
file_hash: 9200f4b7c01ae534db411c2832d0714b6eaa58a9d668730c8aeb9497dccadca2
line: 22
column: 11
function: main
value: (long long )n - (long long )x >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
file_hash: 9200f4b7c01ae534db411c2832d0714b6eaa58a9d668730c8aeb9497dccadca2
line: 22
column: 11
function: main
value: x != 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops.c
file_hash: 9200f4b7c01ae534db411c2832d0714b6eaa58a9d668730c8aeb9497dccadca2
line: 22
column: 11
function: main
value: (((((((((((((((((((((((((((((((((((16385 <= x && (-49153LL + (long long
)x) + (long long )y >= 0LL) && (-49153LL + (long long )n) + (long long )y
>= 0LL) && (-32770LL + (long long )n) + (long long )x >= 0LL) && (1073709055LL
- (long long )x) + (long long )y >= 0LL) && (1073709055LL - (long long )n)
+ (long long )y >= 0LL) && (1073725438LL - (long long )n) + (long long )x
>= 0LL) && (16383LL + (long long )x) - (long long )y >= 0LL) && (16383LL +
(long long )n) - (long long )y >= 0LL) && (1073774591LL - (long long )x) -
(long long )y >= 0LL) && (1073774591LL - (long long )n) - (long long )y >=
0LL) && y == 32768) || (((((((((((8193 <= x && (-24577LL + (long long )x)
+ (long long )y >= 0LL) && (-24577LL + (long long )n) + (long long )y >= 0LL)
&& (-16386LL + (long long )n) + (long long )x >= 0LL) && (1073725439LL - (long
long )x) + (long long )y >= 0LL) && (1073725439LL - (long long )n) + (long
long )y >= 0LL) && (1073733630LL - (long long )n) + (long long )x >= 0LL)
&& (8191LL + (long long )x) - (long long )y >= 0LL) && (8191LL + (long long
)n) - (long long )y >= 0LL) && (1073758207LL - (long long )x) - (long long
)y >= 0LL) && (1073758207LL - (long long )n) - (long long )y >= 0LL) && y
== 16384)) || (((((((((((4097 <= x && (-12289LL + (long long )x) + (long long
)y >= 0LL) && (-12289LL + (long long )n) + (long long )y >= 0LL) && (-8194LL
+ (long long )n) + (long long )x >= 0LL) && (1073733631LL - (long long )x)
+ (long long )y >= 0LL) && (1073733631LL - (long long )n) + (long long )y
>= 0LL) && (1073737726LL - (long long )n) + (long long )x >= 0LL) && (4095LL
+ (long long )x) - (long long )y >= 0LL) && (4095LL + (long long )n) - (long
long )y >= 0LL) && (1073750015LL - (long long )x) - (long long )y >= 0LL)
&& (1073750015LL - (long long )n) - (long long )y >= 0LL) && y == 8192)) ||
(((((((((((2049 <= x && (-6145LL + (long long )x) + (long long )y >= 0LL)
&& (-6145LL + (long long )n) + (long long )y >= 0LL) && (-4098LL + (long long
)n) + (long long )x >= 0LL) && (1073737727LL - (long long )x) + (long long
)y >= 0LL) && (1073737727LL - (long long )n) + (long long )y >= 0LL) && (1073739774LL
- (long long )n) + (long long )x >= 0LL) && (2047LL + (long long )x) - (long
long )y >= 0LL) && (2047LL + (long long )n) - (long long )y >= 0LL) && (1073745919LL
- (long long )x) - (long long )y >= 0LL) && (1073745919LL - (long long )n)
- (long long )y >= 0LL) && y == 4096)) || (((((((((((1025 <= x && (-3073LL
+ (long long )x) + (long long )y >= 0LL) && (-3073LL + (long long )n) + (long
long )y >= 0LL) && (-2050LL + (long long )n) + (long long )x >= 0LL) && (1073739775LL
- (long long )x) + (long long )y >= 0LL) && (1073739775LL - (long long )n)
+ (long long )y >= 0LL) && (1073740798LL - (long long )n) + (long long )x
>= 0LL) && (1023LL + (long long )x) - (long long )y >= 0LL) && (1023LL + (long
long )n) - (long long )y >= 0LL) && (1073743871LL - (long long )x) - (long
long )y >= 0LL) && (1073743871LL - (long long )n) - (long long )y >= 0LL)
&& y == 2048)) || (((((((((((513 <= x && (-1537LL + (long long )x) + (long
long )y >= 0LL) && (-1537LL + (long long )n) + (long long )y >= 0LL) && (-1026LL
+ (long long )n) + (long long )x >= 0LL) && (1073740799LL - (long long )x)
+ (long long )y >= 0LL) && (1073740799LL - (long long )n) + (long long )y
>= 0LL) && (1073741310LL - (long long )n) + (long long )x >= 0LL) && (511LL
+ (long long )x) - (long long )y >= 0LL) && (511LL + (long long )n) - (long
long )y >= 0LL) && (1073742847LL - (long long )x) - (long long )y >= 0LL)
&& (1073742847LL - (long long )n) - (long long )y >= 0LL) && y == 1024)) ||
(((((((((((257 <= x && (-769LL + (long long )x) + (long long )y >= 0LL) &&
(-769LL + (long long )n) + (long long )y >= 0LL) && (-514LL + (long long )n)
+ (long long )x >= 0LL) && (1073741311LL - (long long )x) + (long long )y
>= 0LL) && (1073741311LL - (long long )n) + (long long )y >= 0LL) && (1073741566LL
- (long long )n) + (long long )x >= 0LL) && (255LL + (long long )x) - (long
long )y >= 0LL) && (255LL + (long long )n) - (long long )y >= 0LL) && (1073742335LL
- (long long )x) - (long long )y >= 0LL) && (1073742335LL - (long long )n)
- (long long )y >= 0LL) && y == 512)) || (((((((((((129 <= x && (-385LL +
(long long )x) + (long long )y >= 0LL) && (-385LL + (long long )n) + (long
long )y >= 0LL) && (-258LL + (long long )n) + (long long )x >= 0LL) && (1073741567LL
- (long long )x) + (long long )y >= 0LL) && (1073741567LL - (long long )n)
+ (long long )y >= 0LL) && (1073741694LL - (long long )n) + (long long )x
>= 0LL) && (127LL + (long long )x) - (long long )y >= 0LL) && (127LL + (long
long )n) - (long long )y >= 0LL) && (1073742079LL - (long long )x) - (long
long )y >= 0LL) && (1073742079LL - (long long )n) - (long long )y >= 0LL)
&& y == 256)) || (((((((((((65 <= x && (-193LL + (long long )x) + (long long
)y >= 0LL) && (-193LL + (long long )n) + (long long )y >= 0LL) && (-130LL
+ (long long )n) + (long long )x >= 0LL) && (1073741695LL - (long long )x)
+ (long long )y >= 0LL) && (1073741695LL - (long long )n) + (long long )y
>= 0LL) && (1073741758LL - (long long )n) + (long long )x >= 0LL) && (63LL
+ (long long )x) - (long long )y >= 0LL) && (63LL + (long long )n) - (long
long )y >= 0LL) && (1073741951LL - (long long )x) - (long long )y >= 0LL)
&& (1073741951LL - (long long )n) - (long long )y >= 0LL) && y == 128)) ||
(((((((((((((16777217 <= x && 33554432 <= y) && y <= 2147483644) && (-50331649LL
+ (long long )x) + (long long )y >= 0LL) && (-50331649LL + (long long )n)
+ (long long )y >= 0LL) && (-33554434LL + (long long )n) + (long long )x >=
0LL) && (1040187391LL - (long long )x) + (long long )y >= 0LL) && (1040187391LL
- (long long )n) + (long long )y >= 0LL) && (1056964606LL - (long long )n)
+ (long long )x >= 0LL) && (1073741821LL + (long long )x) - (long long )y
>= 0LL) && (1073741821LL + (long long )n) - (long long )y >= 0LL) && (3221225467LL
- (long long )x) - (long long )y >= 0LL) && (3221225467LL - (long long )n)
- (long long )y >= 0LL) && y % 33554432 == 0)) || (((((((((((33 <= x && (-97LL
+ (long long )x) + (long long )y >= 0LL) && (-97LL + (long long )n) + (long
long )y >= 0LL) && (-66LL + (long long )n) + (long long )x >= 0LL) && (1073741759LL
- (long long )x) + (long long )y >= 0LL) && (1073741759LL - (long long )n)
+ (long long )y >= 0LL) && (1073741790LL - (long long )n) + (long long )x
>= 0LL) && (31LL + (long long )x) - (long long )y >= 0LL) && (31LL + (long
long )n) - (long long )y >= 0LL) && (1073741887LL - (long long )x) - (long
long )y >= 0LL) && (1073741887LL - (long long )n) - (long long )y >= 0LL)
&& y == 64)) || (((((((((((8388609 <= x && (-25165825LL + (long long )x) +
(long long )y >= 0LL) && (-25165825LL + (long long )n) + (long long )y >=
0LL) && (-16777218LL + (long long )n) + (long long )x >= 0LL) && (1056964607LL
- (long long )x) + (long long )y >= 0LL) && (1056964607LL - (long long )n)
+ (long long )y >= 0LL) && (1065353214LL - (long long )n) + (long long )x
>= 0LL) && (8388607LL + (long long )x) - (long long )y >= 0LL) && (8388607LL
+ (long long )n) - (long long )y >= 0LL) && (1090519039LL - (long long )x)
- (long long )y >= 0LL) && (1090519039LL - (long long )n) - (long long )y
>= 0LL) && y == 16777216)) || (((((((((((17 <= x && (-49LL + (long long )x)
+ (long long )y >= 0LL) && (-49LL + (long long )n) + (long long )y >= 0LL)
&& (-34LL + (long long )n) + (long long )x >= 0LL) && (1073741791LL - (long
long )x) + (long long )y >= 0LL) && (1073741791LL - (long long )n) + (long
long )y >= 0LL) && (1073741806LL - (long long )n) + (long long )x >= 0LL)
&& (15LL + (long long )x) - (long long )y >= 0LL) && (15LL + (long long )n)
- (long long )y >= 0LL) && (1073741855LL - (long long )x) - (long long )y
>= 0LL) && (1073741855LL - (long long )n) - (long long )y >= 0LL) && y ==
32)) || (((((((((((4194305 <= x && (-12582913LL + (long long )x) + (long long
)y >= 0LL) && (-12582913LL + (long long )n) + (long long )y >= 0LL) && (-8388610LL
+ (long long )n) + (long long )x >= 0LL) && (1065353215LL - (long long )x)
+ (long long )y >= 0LL) && (1065353215LL - (long long )n) + (long long )y
>= 0LL) && (1069547518LL - (long long )n) + (long long )x >= 0LL) && (4194303LL
+ (long long )x) - (long long )y >= 0LL) && (4194303LL + (long long )n) -
(long long )y >= 0LL) && (1082130431LL - (long long )x) - (long long )y >=
0LL) && (1082130431LL - (long long )n) - (long long )y >= 0LL) && y == 8388608))
|| (((((((((((9 <= x && (-25LL + (long long )x) + (long long )y >= 0LL) &&
(-25LL + (long long )n) + (long long )y >= 0LL) && (-18LL + (long long )n)
+ (long long )x >= 0LL) && (1073741807LL - (long long )x) + (long long )y
>= 0LL) && (1073741807LL - (long long )n) + (long long )y >= 0LL) && (1073741814LL
- (long long )n) + (long long )x >= 0LL) && (7LL + (long long )x) - (long
long )y >= 0LL) && (7LL + (long long )n) - (long long )y >= 0LL) && (1073741839LL
- (long long )x) - (long long )y >= 0LL) && (1073741839LL - (long long )n)
- (long long )y >= 0LL) && y == 16)) || (((((((((((2097153 <= x && (-6291457LL
+ (long long )x) + (long long )y >= 0LL) && (-6291457LL + (long long )n) +
(long long )y >= 0LL) && (-4194306LL + (long long )n) + (long long )x >= 0LL)
&& (1069547519LL - (long long )x) + (long long )y >= 0LL) && (1069547519LL
- (long long )n) + (long long )y >= 0LL) && (1071644670LL - (long long )n)
+ (long long )x >= 0LL) && (2097151LL + (long long )x) - (long long )y >=
0LL) && (2097151LL + (long long )n) - (long long )y >= 0LL) && (1077936127LL
- (long long )x) - (long long )y >= 0LL) && (1077936127LL - (long long )n)
- (long long )y >= 0LL) && y == 4194304)) || (((((((((((5 <= x && (-13LL +
(long long )x) + (long long )y >= 0LL) && (-13LL + (long long )n) + (long
long )y >= 0LL) && (-10LL + (long long )n) + (long long )x >= 0LL) && (1073741815LL
- (long long )x) + (long long )y >= 0LL) && (1073741815LL - (long long )n)
+ (long long )y >= 0LL) && (1073741818LL - (long long )n) + (long long )x
>= 0LL) && (3LL + (long long )x) - (long long )y >= 0LL) && (3LL + (long long
)n) - (long long )y >= 0LL) && (1073741831LL - (long long )x) - (long long
)y >= 0LL) && (1073741831LL - (long long )n) - (long long )y >= 0LL) && y
== 8)) || (((((((((((1048577 <= x && (-3145729LL + (long long )x) + (long
long )y >= 0LL) && (-3145729LL + (long long )n) + (long long )y >= 0LL) &&
(-2097154LL + (long long )n) + (long long )x >= 0LL) && (1071644671LL - (long
long )x) + (long long )y >= 0LL) && (1071644671LL - (long long )n) + (long
long )y >= 0LL) && (1072693246LL - (long long )n) + (long long )x >= 0LL)
&& (1048575LL + (long long )x) - (long long )y >= 0LL) && (1048575LL + (long
long )n) - (long long )y >= 0LL) && (1075838975LL - (long long )x) - (long
long )y >= 0LL) && (1075838975LL - (long long )n) - (long long )y >= 0LL)
&& y == 2097152)) || (((((((((((3 <= x && (-7LL + (long long )x) + (long long
)y >= 0LL) && (-7LL + (long long )n) + (long long )y >= 0LL) && (-6LL + (long
long )n) + (long long )x >= 0LL) && (1073741819LL - (long long )x) + (long
long )y >= 0LL) && (1073741819LL - (long long )n) + (long long )y >= 0LL)
&& (1073741820LL - (long long )n) + (long long )x >= 0LL) && (1LL + (long
long )x) - (long long )y >= 0LL) && (1LL + (long long )n) - (long long )y
>= 0LL) && (1073741827LL - (long long )x) - (long long )y >= 0LL) && (1073741827LL
- (long long )n) - (long long )y >= 0LL) && y == 4)) || (((((((((((524289
<= x && (-1572865LL + (long long )x) + (long long )y >= 0LL) && (-1572865LL
+ (long long )n) + (long long )y >= 0LL) && (-1048578LL + (long long )n) +
(long long )x >= 0LL) && (1072693247LL - (long long )x) + (long long )y >=
0LL) && (1072693247LL - (long long )n) + (long long )y >= 0LL) && (1073217534LL
- (long long )n) + (long long )x >= 0LL) && (524287LL + (long long )x) - (long
long )y >= 0LL) && (524287LL + (long long )n) - (long long )y >= 0LL) && (1074790399LL
- (long long )x) - (long long )y >= 0LL) && (1074790399LL - (long long )n)
- (long long )y >= 0LL) && y == 1048576)) || (((((((((((2 <= x && (-4LL +
(long long )x) + (long long )y >= 0LL) && (-4LL + (long long )n) + (long long
)x >= 0LL) && (-4LL + (long long )n) + (long long )y >= 0LL) && (1073741821LL
- (long long )x) + (long long )y >= 0LL) && (1073741821LL - (long long )n)
+ (long long )x >= 0LL) && (1073741821LL - (long long )n) + (long long )y
>= 0LL) && (1073741825LL - (long long )x) - (long long )y >= 0LL) && (1073741825LL
- (long long )n) - (long long )y >= 0LL) && (long long )x - (long long )y
>= 0LL) && (long long )n - (long long )y >= 0LL) && y == 2)) || (((((((((((262145
<= x && (-786433LL + (long long )x) + (long long )y >= 0LL) && (-786433LL
+ (long long )n) + (long long )y >= 0LL) && (-524290LL + (long long )n) +
(long long )x >= 0LL) && (1073217535LL - (long long )x) + (long long )y >=
0LL) && (1073217535LL - (long long )n) + (long long )y >= 0LL) && (1073479678LL
- (long long )n) + (long long )x >= 0LL) && (262143LL + (long long )x) - (long
long )y >= 0LL) && (262143LL + (long long )n) - (long long )y >= 0LL) && (1074266111LL
- (long long )x) - (long long )y >= 0LL) && (1074266111LL - (long long )n)
- (long long )y >= 0LL) && y == 524288)) || ((((((((((((2 <= x && (-4LL +
(long long )n) + (long long )x >= 0LL) && (-3LL + (long long )x) + (long long
)y >= 0LL) && (-3LL + (long long )n) + (long long )y >= 0LL) && (1073741821LL
- (long long )n) + (long long )x >= 0LL) && (1073741822LL - (long long )x)
+ (long long )y >= 0LL) && (1073741822LL - (long long )n) + (long long )y
>= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && (-1LL + (long
long )n) - (long long )y >= 0LL) && (1073741824LL - (long long )x) - (long
long )y >= 0LL) && (1073741824LL - (long long )n) - (long long )y >= 0LL)
&& 1 == y) && y == 1)) || (((((((((((131073 <= x && (-393217LL + (long long
)x) + (long long )y >= 0LL) && (-393217LL + (long long )n) + (long long )y
>= 0LL) && (-262146LL + (long long )n) + (long long )x >= 0LL) && (1073479679LL
- (long long )x) + (long long )y >= 0LL) && (1073479679LL - (long long )n)
+ (long long )y >= 0LL) && (1073610750LL - (long long )n) + (long long )x
>= 0LL) && (131071LL + (long long )x) - (long long )y >= 0LL) && (131071LL
+ (long long )n) - (long long )y >= 0LL) && (1074003967LL - (long long )x)
- (long long )y >= 0LL) && (1074003967LL - (long long )n) - (long long )y
>= 0LL) && y == 262144)) || (((((((((((65537 <= x && (-196609LL + (long long
)x) + (long long )y >= 0LL) && (-196609LL + (long long )n) + (long long )y
>= 0LL) && (-131074LL + (long long )n) + (long long )x >= 0LL) && (1073610751LL
- (long long )x) + (long long )y >= 0LL) && (1073610751LL - (long long )n)
+ (long long )y >= 0LL) && (1073676286LL - (long long )n) + (long long )x
>= 0LL) && (65535LL + (long long )x) - (long long )y >= 0LL) && (65535LL +
(long long )n) - (long long )y >= 0LL) && (1073872895LL - (long long )x) -
(long long )y >= 0LL) && (1073872895LL - (long long )n) - (long long )y >=
0LL) && y == 131072)) || (((((((((((32769 <= x && (-98305LL + (long long )x)
+ (long long )y >= 0LL) && (-98305LL + (long long )n) + (long long )y >= 0LL)
&& (-65538LL + (long long )n) + (long long )x >= 0LL) && (1073676287LL - (long
long )x) + (long long )y >= 0LL) && (1073676287LL - (long long )n) + (long
long )y >= 0LL) && (1073709054LL - (long long )n) + (long long )x >= 0LL)
&& (32767LL + (long long )x) - (long long )y >= 0LL) && (32767LL + (long long
)n) - (long long )y >= 0LL) && (1073807359LL - (long long )x) - (long long
)y >= 0LL) && (1073807359LL - (long long )n) - (long long )y >= 0LL) && y
== 65536)
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
31 |
2023-12-01T04:30:00+01:00 |
|