6a989e4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T07:22:12Z |
|
d7648b4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T17:46:00+01:00 |
|
57b7e57 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:37 CET (comp) |
|
ceabdb1 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
8 |
2023-12-02T11:36:50Z |
|
b4f88eb |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Mopsa (v1.0~pre2) |
3 |
2023-11-29T06:19:32Z |
|
218a762 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Kojak |
8 |
2023-12-03T01:19:40Z |
|
5d68ee4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
40 |
2023-12-01T00:59:27Z |
|
cfdbc59 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-20T03:41:13+01:00 |
57b7e57 |
49426d0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-19T14:28:27+01:00 |
ea053b7 |
44cffa0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-19T03:12:37+01:00 |
2255f62 |
ca6a5aa |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-17T06:10:29+01:00 |
a1f016c |
55184e8 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-04T11:39:09+01:00 |
ceabdb1 |
22ffae6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-04T01:42:53+01:00 |
6d72e20 |
b716337 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-03T18:32:01+01:00 |
d7648b4 |
609f7ce |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-03T09:58:56+01:00 |
6a989e4 |
11032c0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-03T06:01:38+01:00 |
218a762 |
93152b6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-01T03:54:04+01:00 |
5d68ee4 |
d4bd2b4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-01T00:18:15+01:00 |
3d24f4c |
e06c4c5 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-11-30T13:00:43+01:00 |
b4e5b1a |
b4e5b1a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-11-30T05:28:58+01:00 |
|
1112701 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-11-29T18:35:09+01:00 |
b4f88eb |
92ad338 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-11-29T08:09:51+01:00 |
e406789 |
6d72e20 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
6 |
2023-12-03T22:10:35+01:00 |
|
a1f016c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.1 |
6 |
2023-12-17T03:44:58+01:00 |
|
2255f62 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
6 |
2023-12-18T19:33:36+01:00 |
|
e406789 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
8 |
2023-11-29T02:07:33Z |
|
3d24f4c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
2LS |
9 |
2023-11-30T21:32:46+01:00 |
|
2cd5630 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
2LS |
9 |
2023-11-30T23:16:59+01:00 |
|
6b31ab3 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: f3b45f6b-f26b-489c-805a-6d338eb401ad
creation_time: '2023-12-02T12:36:50+01:00'
producer:
name: Taipan
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_1220027c-0efe-4669-a729-949d52462b91/sv-benchmarks/c/termination-restricted-15/b.18.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_1220027c-0efe-4669-a729-949d52462b91/sv-benchmarks/c/termination-restricted-15/b.18.c
: b7b84dd29ea36609e5f5c61ea995baac9099f3fa2331fbdc558930ff5215a280
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_1220027c-0efe-4669-a729-949d52462b91/sv-benchmarks/c/termination-restricted-15/b.18.c
file_hash: b7b84dd29ea36609e5f5c61ea995baac9099f3fa2331fbdc558930ff5215a280
line: 9
column: 0
function: main
value: ((x <= 2147483647) && (y <= 2147483647))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_1220027c-0efe-4669-a729-949d52462b91/sv-benchmarks/c/termination-restricted-15/b.18.c
file_hash: b7b84dd29ea36609e5f5c61ea995baac9099f3fa2331fbdc558930ff5215a280
line: 11
column: 0
function: main
value: (((1 <= y) && (x <= 2147483647)) && (y <= 2147483647))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_1220027c-0efe-4669-a729-949d52462b91/sv-benchmarks/c/termination-restricted-15/b.18.c
file_hash: b7b84dd29ea36609e5f5c61ea995baac9099f3fa2331fbdc558930ff5215a280
line: 15
column: 0
function: main
value: (((x <= 2147483647) && (1 <= x)) && (y <= 2147483647))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-04T11:59:33+01:00 |
|
7c60a54 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: dc4de49f-dd25-4a33-b6de-827fb5ca72b6
creation_time: '2023-11-29T03:07:33+01:00'
producer:
name: Automizer
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_051a89f1-bacf-46e6-88fb-08a4ade9ddc2/sv-benchmarks/c/termination-restricted-15/b.18.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_051a89f1-bacf-46e6-88fb-08a4ade9ddc2/sv-benchmarks/c/termination-restricted-15/b.18.c
: b7b84dd29ea36609e5f5c61ea995baac9099f3fa2331fbdc558930ff5215a280
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_051a89f1-bacf-46e6-88fb-08a4ade9ddc2/sv-benchmarks/c/termination-restricted-15/b.18.c
file_hash: b7b84dd29ea36609e5f5c61ea995baac9099f3fa2331fbdc558930ff5215a280
line: 9
column: 0
function: main
value: ((x <= 2147483647) && (y <= 2147483647))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_051a89f1-bacf-46e6-88fb-08a4ade9ddc2/sv-benchmarks/c/termination-restricted-15/b.18.c
file_hash: b7b84dd29ea36609e5f5c61ea995baac9099f3fa2331fbdc558930ff5215a280
line: 11
column: 0
function: main
value: (((1 <= y) && (x <= 2147483647)) && (y <= 2147483647))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_051a89f1-bacf-46e6-88fb-08a4ade9ddc2/sv-benchmarks/c/termination-restricted-15/b.18.c
file_hash: b7b84dd29ea36609e5f5c61ea995baac9099f3fa2331fbdc558930ff5215a280
line: 15
column: 0
function: main
value: (((x <= 2147483647) && (1 <= x)) && (y <= 2147483647))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-29T07:48:49+01:00 |
|
ac2ca18 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: bf0c224c-2ce3-423b-8aeb-de36f046b827
creation_time: '2023-12-03T02:19:40+01:00'
producer:
name: Kojak
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_160d1543-3c5a-4567-af84-c2daca2b7a93/sv-benchmarks/c/termination-restricted-15/b.18.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_160d1543-3c5a-4567-af84-c2daca2b7a93/sv-benchmarks/c/termination-restricted-15/b.18.c
: b7b84dd29ea36609e5f5c61ea995baac9099f3fa2331fbdc558930ff5215a280
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_160d1543-3c5a-4567-af84-c2daca2b7a93/sv-benchmarks/c/termination-restricted-15/b.18.c
file_hash: b7b84dd29ea36609e5f5c61ea995baac9099f3fa2331fbdc558930ff5215a280
line: 9
column: 0
function: main
value: (((x < 1) || (y < 1)) || ((x <= 2147483647) && (y <= 2147483647)))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_160d1543-3c5a-4567-af84-c2daca2b7a93/sv-benchmarks/c/termination-restricted-15/b.18.c
file_hash: b7b84dd29ea36609e5f5c61ea995baac9099f3fa2331fbdc558930ff5215a280
line: 11
column: 0
function: main
value: (x <= 2147483647)
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_160d1543-3c5a-4567-af84-c2daca2b7a93/sv-benchmarks/c/termination-restricted-15/b.18.c
file_hash: b7b84dd29ea36609e5f5c61ea995baac9099f3fa2331fbdc558930ff5215a280
line: 15
column: 0
function: main
value: (y <= 2147483647)
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-03T05:38:51+01:00 |
|
9c3d08a |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: f7f2dde4-545c-4821-a9d3-6792a7b35fcf
creation_time: 2023-12-01T00:59:27Z
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-restricted-15/b.18.c'''
task:
input_files:
- ../../sv-benchmarks/c/termination-restricted-15/b.18.c
input_file_hashes:
../../sv-benchmarks/c/termination-restricted-15/b.18.c: b7b84dd29ea36609e5f5c61ea995baac9099f3fa2331fbdc558930ff5215a280
data_model: LP64
language: C
specification: CHECK( init(main()), LTL(G ! overflow) )
content:
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/b.18.c
file_hash: b7b84dd29ea36609e5f5c61ea995baac9099f3fa2331fbdc558930ff5215a280
line: 15
column: 19
function: main
value: 1 <= x
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/b.18.c
file_hash: b7b84dd29ea36609e5f5c61ea995baac9099f3fa2331fbdc558930ff5215a280
line: 15
column: 19
function: main
value: x != 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/b.18.c
file_hash: b7b84dd29ea36609e5f5c61ea995baac9099f3fa2331fbdc558930ff5215a280
line: 15
column: 19
function: main
value: (((((((((((((0 <= y && (-1LL + (long long )x) + (long long )y >= 0LL)
&& y != -1) && (((y != -2 && (((y != -3 && (((y != -4 && (((y != -5 && (((y
!= -6 && (((y != -7 && ((((y <= 2147483639 && (8LL - (long long )x) + (long
long )y >= 0LL) && y != -8) || (y <= 2147483640 && (7LL - (long long )x) +
(long long )y >= 0LL)) || ((((((((((((((((((y <= 2147483622 && y != -25) &&
y != -24) && y != -23) && y != -22) && y != -21) && y != -20) && y != -19)
&& y != -18) && y != -17) && y != -16) && y != -15) && y != -14) && y != -13)
&& y != -12) && y != -11) && y != -10) && y != -9) && y != -8))) || (y <=
2147483641 && (6LL - (long long )x) + (long long )y >= 0LL)) || (((((((((((((((((((y
<= 2147483623 && (24LL - (long long )x) + (long long )y >= 0LL) && y != -24)
&& y != -23) && y != -22) && y != -21) && y != -20) && y != -19) && y != -18)
&& y != -17) && y != -16) && y != -15) && y != -14) && y != -13) && y != -12)
&& y != -11) && y != -10) && y != -9) && y != -8) && y != -7))) || (y <= 2147483642
&& (5LL - (long long )x) + (long long )y >= 0LL)) || (((((((((((((((((((y
<= 2147483624 && (23LL - (long long )x) + (long long )y >= 0LL) && y != -23)
&& y != -22) && y != -21) && y != -20) && y != -19) && y != -18) && y != -17)
&& y != -16) && y != -15) && y != -14) && y != -13) && y != -12) && y != -11)
&& y != -10) && y != -9) && y != -8) && y != -7) && y != -6))) || (y <= 2147483643
&& (4LL - (long long )x) + (long long )y >= 0LL)) || (((((((((((((((((((y
<= 2147483625 && (22LL - (long long )x) + (long long )y >= 0LL) && y != -22)
&& y != -21) && y != -20) && y != -19) && y != -18) && y != -17) && y != -16)
&& y != -15) && y != -14) && y != -13) && y != -12) && y != -11) && y != -10)
&& y != -9) && y != -8) && y != -7) && y != -6) && y != -5))) || (y <= 2147483644
&& (3LL - (long long )x) + (long long )y >= 0LL)) || (((((((((((((((((((y
<= 2147483626 && (21LL - (long long )x) + (long long )y >= 0LL) && y != -21)
&& y != -20) && y != -19) && y != -18) && y != -17) && y != -16) && y != -15)
&& y != -14) && y != -13) && y != -12) && y != -11) && y != -10) && y != -9)
&& y != -8) && y != -7) && y != -6) && y != -5) && y != -4))) || (y <= 2147483645
&& (2LL - (long long )x) + (long long )y >= 0LL)) || (((((((((((((((((((y
<= 2147483627 && (20LL - (long long )x) + (long long )y >= 0LL) && y != -20)
&& y != -19) && y != -18) && y != -17) && y != -16) && y != -15) && y != -14)
&& y != -13) && y != -12) && y != -11) && y != -10) && y != -9) && y != -8)
&& y != -7) && y != -6) && y != -5) && y != -4) && y != -3))) || (y <= 2147483646
&& (1LL - (long long )x) + (long long )y >= 0LL)) || (((((((((((((((((((y
<= 2147483628 && (19LL - (long long )x) + (long long )y >= 0LL) && y != -19)
&& y != -18) && y != -17) && y != -16) && y != -15) && y != -14) && y != -13)
&& y != -12) && y != -11) && y != -10) && y != -9) && y != -8) && y != -7)
&& y != -6) && y != -5) && y != -4) && y != -3) && y != -2))) || (((1 <= y
&& (-2LL + (long long )x) + (long long )y >= 0LL) && (0LL - (long long )x)
+ (long long )y >= 0LL) && y != 0)) || (((((((((((((((((((((0 <= y && y <=
2147483629) && (-1LL + (long long )x) + (long long )y >= 0LL) && (18LL - (long
long )x) + (long long )y >= 0LL) && y != -18) && y != -17) && y != -16) &&
y != -15) && y != -14) && y != -13) && y != -12) && y != -11) && y != -10)
&& y != -9) && y != -8) && y != -7) && y != -6) && y != -5) && y != -4) &&
y != -3) && y != -2) && y != -1)) || ((((((((((((((((((((0 <= y && y <= 2147483630)
&& (-1LL + (long long )x) + (long long )y >= 0LL) && (17LL - (long long )x)
+ (long long )y >= 0LL) && y != -17) && y != -16) && y != -15) && y != -14)
&& y != -13) && y != -12) && y != -11) && y != -10) && y != -9) && y != -8)
&& y != -7) && y != -6) && y != -5) && y != -4) && y != -3) && y != -2) &&
y != -1)) || (((((((((((((((((((0 <= y && y <= 2147483631) && (-1LL + (long
long )x) + (long long )y >= 0LL) && (16LL - (long long )x) + (long long )y
>= 0LL) && y != -16) && y != -15) && y != -14) && y != -13) && y != -12) &&
y != -11) && y != -10) && y != -9) && y != -8) && y != -7) && y != -6) &&
y != -5) && y != -4) && y != -3) && y != -2) && y != -1)) || ((((((((((((((((((0
<= y && y <= 2147483632) && (-1LL + (long long )x) + (long long )y >= 0LL)
&& (15LL - (long long )x) + (long long )y >= 0LL) && y != -15) && y != -14)
&& y != -13) && y != -12) && y != -11) && y != -10) && y != -9) && y != -8)
&& y != -7) && y != -6) && y != -5) && y != -4) && y != -3) && y != -2) &&
y != -1)) || (((((((((((((((((0 <= y && y <= 2147483633) && (-1LL + (long
long )x) + (long long )y >= 0LL) && (14LL - (long long )x) + (long long )y
>= 0LL) && y != -14) && y != -13) && y != -12) && y != -11) && y != -10) &&
y != -9) && y != -8) && y != -7) && y != -6) && y != -5) && y != -4) && y
!= -3) && y != -2) && y != -1)) || ((((((((((((((((0 <= y && y <= 2147483634)
&& (-1LL + (long long )x) + (long long )y >= 0LL) && (13LL - (long long )x)
+ (long long )y >= 0LL) && y != -13) && y != -12) && y != -11) && y != -10)
&& y != -9) && y != -8) && y != -7) && y != -6) && y != -5) && y != -4) &&
y != -3) && y != -2) && y != -1)) || (((((((((((((((0 <= y && y <= 2147483635)
&& (-1LL + (long long )x) + (long long )y >= 0LL) && (12LL - (long long )x)
+ (long long )y >= 0LL) && y != -12) && y != -11) && y != -10) && y != -9)
&& y != -8) && y != -7) && y != -6) && y != -5) && y != -4) && y != -3) &&
y != -2) && y != -1)) || ((((((((((((((0 <= y && y <= 2147483636) && (-1LL
+ (long long )x) + (long long )y >= 0LL) && (11LL - (long long )x) + (long
long )y >= 0LL) && y != -11) && y != -10) && y != -9) && y != -8) && y !=
-7) && y != -6) && y != -5) && y != -4) && y != -3) && y != -2) && y != -1))
|| (((((((((((((0 <= y && y <= 2147483637) && (-1LL + (long long )x) + (long
long )y >= 0LL) && (10LL - (long long )x) + (long long )y >= 0LL) && y !=
-10) && y != -9) && y != -8) && y != -7) && y != -6) && y != -5) && y != -4)
&& y != -3) && y != -2) && y != -1)) || ((((((((((((0 <= y && y <= 2147483638)
&& (-1LL + (long long )x) + (long long )y >= 0LL) && (9LL - (long long )x)
+ (long long )y >= 0LL) && y != -9) && y != -8) && y != -7) && y != -6) &&
y != -5) && y != -4) && y != -3) && y != -2) && y != -1)
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/b.18.c
file_hash: b7b84dd29ea36609e5f5c61ea995baac9099f3fa2331fbdc558930ff5215a280
line: 11
column: 19
function: main
value: 1 <= y
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/b.18.c
file_hash: b7b84dd29ea36609e5f5c61ea995baac9099f3fa2331fbdc558930ff5215a280
line: 11
column: 19
function: main
value: y <= 2147483646
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/b.18.c
file_hash: b7b84dd29ea36609e5f5c61ea995baac9099f3fa2331fbdc558930ff5215a280
line: 11
column: 19
function: main
value: y != 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/b.18.c
file_hash: b7b84dd29ea36609e5f5c61ea995baac9099f3fa2331fbdc558930ff5215a280
line: 11
column: 19
function: main
value: (((x != -1 && (((((0 <= x && (-1LL + (long long )x) + (long long )y >=
0LL) && x != -2) && (((x != -3 && (((x != -4 && (((x != -5 && (((x != -6 &&
(((x != -7 && (((x != -8 && ((x != -9 && ((x != -10 && ((x != -11 && ((x !=
-12 && ((x != -13 && ((x != -14 && ((x != -15 && (((x <= 2147483631 && (15LL
+ (long long )x) - (long long )y >= 0LL) && x != -16) || (x <= 2147483632
&& (14LL + (long long )x) - (long long )y >= 0LL))) || (x <= 2147483633 &&
(13LL + (long long )x) - (long long )y >= 0LL))) || (x <= 2147483634 && (12LL
+ (long long )x) - (long long )y >= 0LL))) || (x <= 2147483635 && (11LL +
(long long )x) - (long long )y >= 0LL))) || (x <= 2147483636 && (10LL + (long
long )x) - (long long )y >= 0LL))) || (x <= 2147483637 && (9LL + (long long
)x) - (long long )y >= 0LL))) || (x <= 2147483638 && (8LL + (long long )x)
- (long long )y >= 0LL))) || (x <= 2147483639 && (7LL + (long long )x) - (long
long )y >= 0LL))) || (x <= 2147483640 && (6LL + (long long )x) - (long long
)y >= 0LL)) || ((((((((((((((((((x <= 2147483622 && x != -25) && x != -24)
&& x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18)
&& x != -17) && x != -16) && x != -15) && x != -14) && x != -13) && x != -12)
&& x != -11) && x != -10) && x != -9) && x != -8))) || (x <= 2147483641 &&
(5LL + (long long )x) - (long long )y >= 0LL)) || (((((((((((((((((((x <=
2147483623 && (23LL + (long long )x) - (long long )y >= 0LL) && x != -24)
&& x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18)
&& x != -17) && x != -16) && x != -15) && x != -14) && x != -13) && x != -12)
&& x != -11) && x != -10) && x != -9) && x != -8) && x != -7))) || (x <= 2147483642
&& (4LL + (long long )x) - (long long )y >= 0LL)) || (((((((((((((((((((x
<= 2147483624 && (22LL + (long long )x) - (long long )y >= 0LL) && x != -23)
&& x != -22) && x != -21) && x != -20) && x != -19) && x != -18) && x != -17)
&& x != -16) && x != -15) && x != -14) && x != -13) && x != -12) && x != -11)
&& x != -10) && x != -9) && x != -8) && x != -7) && x != -6))) || (x <= 2147483643
&& (3LL + (long long )x) - (long long )y >= 0LL)) || (((((((((((((((((((x
<= 2147483625 && (21LL + (long long )x) - (long long )y >= 0LL) && x != -22)
&& x != -21) && x != -20) && x != -19) && x != -18) && x != -17) && x != -16)
&& x != -15) && x != -14) && x != -13) && x != -12) && x != -11) && x != -10)
&& x != -9) && x != -8) && x != -7) && x != -6) && x != -5))) || (x <= 2147483644
&& (2LL + (long long )x) - (long long )y >= 0LL)) || (((((((((((((((((((x
<= 2147483626 && (20LL + (long long )x) - (long long )y >= 0LL) && x != -21)
&& x != -20) && x != -19) && x != -18) && x != -17) && x != -16) && x != -15)
&& x != -14) && x != -13) && x != -12) && x != -11) && x != -10) && x != -9)
&& x != -8) && x != -7) && x != -6) && x != -5) && x != -4))) || (x <= 2147483645
&& (1LL + (long long )x) - (long long )y >= 0LL)) || (((((((((((((((((((x
<= 2147483627 && (19LL + (long long )x) - (long long )y >= 0LL) && x != -20)
&& x != -19) && x != -18) && x != -17) && x != -16) && x != -15) && x != -14)
&& x != -13) && x != -12) && x != -11) && x != -10) && x != -9) && x != -8)
&& x != -7) && x != -6) && x != -5) && x != -4) && x != -3))) || (((1 <= x
&& x <= 2147483646) && (-2LL + (long long )x) + (long long )y >= 0LL) && (long
long )x - (long long )y >= 0LL)) || (((((((((((((((((((((0 <= x && x <= 2147483628)
&& (-1LL + (long long )x) + (long long )y >= 0LL) && (18LL + (long long )x)
- (long long )y >= 0LL) && x != -19) && x != -18) && x != -17) && x != -16)
&& x != -15) && x != -14) && x != -13) && x != -12) && x != -11) && x != -10)
&& x != -9) && x != -8) && x != -7) && x != -6) && x != -5) && x != -4) &&
x != -3) && x != -2))) || (((2 <= x && (-3LL + (long long )x) + (long long
)y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && x != 0)) ||
(((((((((((((((((((((0 <= x && x <= 2147483629) && (-1LL + (long long )x)
+ (long long )y >= 0LL) && (17LL + (long long )x) - (long long )y >= 0LL)
&& x != -18) && x != -17) && x != -16) && x != -15) && x != -14) && x != -13)
&& x != -12) && x != -11) && x != -10) && x != -9) && x != -8) && x != -7)
&& x != -6) && x != -5) && x != -4) && x != -3) && x != -2) && x != -1)) ||
((((((((((((((((((((0 <= x && x <= 2147483630) && (-1LL + (long long )x) +
(long long )y >= 0LL) && (16LL + (long long )x) - (long long )y >= 0LL) &&
x != -17) && x != -16) && x != -15) && x != -14) && x != -13) && x != -12)
&& x != -11) && x != -10) && x != -9) && x != -8) && x != -7) && x != -6)
&& x != -5) && x != -4) && x != -3) && x != -2) && x != -1)
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
26 |
2023-12-01T04:27:34+01:00 |
|