82a5b8c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.3 |
6 |
2023-12-04T01:19:05+01:00 |
507169c |
7b672cc |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.3 |
6 |
2023-11-30T12:02:08+01:00 |
769c46d |
bfccbf7 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.1 |
4 |
2023-12-17T03:43:06+01:00 |
|
0801e0e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.0 |
4 |
2023-12-19T12:01:55+01:00 |
|
44ec720 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
4 |
2023-12-18T20:35:43+01:00 |
|
c3b8a9b |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T17:22:14+01:00 |
|
c80f4c7 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T08:06:22Z |
|
5a93caa |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
15 |
2023-12-02T17:19:55Z |
|
a5a08c6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Mopsa (v1.0~pre2) |
3 |
2023-11-29T09:51:41Z |
|
a28f511 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
25 |
2023-12-01T01:16:02Z |
|
1f991c8 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-19T15:34:13+01:00 |
0801e0e |
6f19ed2 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-19T05:26:36+01:00 |
44ec720 |
e4ebdcb |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-17T06:38:08+01:00 |
bfccbf7 |
8d3ecc9 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-04T11:38:25+01:00 |
5a93caa |
e9c85bd |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-03T18:31:06+01:00 |
c3b8a9b |
75538ac |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-03T09:54:38+01:00 |
c80f4c7 |
d707b26 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-01T03:42:06+01:00 |
a28f511 |
769c46d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-11-30T08:14:45+01:00 |
|
41bacbe |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-11-29T18:11:49+01:00 |
a5a08c6 |
4eda49d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-11-29T08:07:17+01:00 |
4634e0d |
507169c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
7 |
2023-12-03T21:09:39+01:00 |
|
4634e0d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
15 |
2023-11-28T23:31:16Z |
|
cb833e9 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
3 |
2023-12-01T01:12:52Z |
|
0757701 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: a50f1aca-0277-4112-95b7-8fb6d91ffdb4
creation_time: '2023-12-02T18:19:55+01:00'
producer:
name: Taipan
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7c84cb03-fdef-4967-9ba4-502124e92a54/sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7c84cb03-fdef-4967-9ba4-502124e92a54/sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i
: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d
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_7c84cb03-fdef-4967-9ba4-502124e92a54/sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i
file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d
line: 550
column: 0
function: SelectionSort
value: ((((i == 0) && (array_size <= 2147483647)) && (1 <= array_size)) || ((((array_size <= 2147483647) && (0 <= (j + 2147483648))) && (1 <= i)) && (1 <= array_size)))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7c84cb03-fdef-4967-9ba4-502124e92a54/sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i
file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d
line: 554
column: 0
function: SelectionSort
value: (((((array_size <= 2147483647) && ((i + 2) <= array_size)) && (0 <= (j + 2147483648))) && (1 <= i)) || ((((i == 0) && (array_size <= 2147483647)) && (1 <= j)) && (2 <= array_size)))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
9 |
2023-12-04T11:59:55+01:00 |
|
96a6434 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 2094a042-e363-495e-811a-a5e72c9f8a09
creation_time: '2023-11-29T00:31:16+01:00'
producer:
name: Automizer
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11763872-a760-4b7f-810a-bc766de6bb73/sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11763872-a760-4b7f-810a-bc766de6bb73/sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i
: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d
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_11763872-a760-4b7f-810a-bc766de6bb73/sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i
file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d
line: 550
column: 0
function: SelectionSort
value: (((((((array_size <= 2147483647) && (array_size <= 2147483647)) && (0 <= (j + 2147483648))) && (1 <= i)) && (1 <= array_size)) && (1 <= array_size)) || (((((i == 0) && (array_size <= 2147483647)) && (array_size <= 2147483647)) && (1 <= array_size)) && (1 <= array_size)))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11763872-a760-4b7f-810a-bc766de6bb73/sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i
file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d
line: 554
column: 0
function: SelectionSort
value: ((((((((i == 0) && (array_size <= 2147483647)) && (array_size <= 2147483647)) && ((i + 2) <= array_size)) && (1 <= j)) && (1 <= array_size)) && (1 <= array_size)) || (((((((array_size <= 2147483647) && (array_size <= 2147483647)) && ((i + 2) <= array_size)) && (0 <= (j + 2147483648))) && (1 <= i)) && (1 <= array_size)) && (1 <= array_size)))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
10 |
2023-11-29T07:49:19+01:00 |
|
dd639ff |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: 9a906ecd-01e7-4fce-b1b9-edaadd554843
creation_time: 2023-12-01T01:16:02Z
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-memory-alloca/selectionsort-alloca-2.i'''
task:
input_files:
- ../../sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i
input_file_hashes:
../../sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d
data_model: LP64
language: C
specification: CHECK( init(main()), LTL(G ! overflow) )
content:
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i
file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d
line: 550
column: 8
function: SelectionSort
value: array_size != 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i
file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d
line: 550
column: 8
function: SelectionSort
value: (0 <= i && ((((((((((((((0 <= min && 2 <= array_size) && 2 <= j) && i
<= 2147483645) && (-4LL + (long long )array_size) + (long long )j >= 0LL)
&& (-2LL + (long long )array_size) + (long long )i >= 0LL) && (-2LL + (long
long )i) + (long long )j >= 0LL) && (-2LL - (long long )i) + (long long )j
>= 0LL) && (0LL - (long long )array_size) + (long long )j >= 0LL) && (-2LL
+ (long long )array_size) - (long long )i >= 0LL) && (long long )array_size
- (long long )j >= 0LL) && array_size != 1) && j != 0) && j != 1) || (((((((1
<= array_size && i <= 2147483646) && (-1LL + (long long )array_size) + (long
long )i >= 0LL) && (2147483647LL + (long long )array_size) + (long long )j
>= 0LL) && (2147483648LL + (long long )i) + (long long )j >= 0LL) && (2147483648LL
- (long long )i) + (long long )j >= 0LL) && (-1LL + (long long )array_size)
- (long long )i >= 0LL) && (2147483646LL + (long long )array_size) - (long
long )j >= 0LL))) || ((((((((((((((((((1 <= array_size && (2147483647LL +
(long long )array_size) + (long long )i >= 0LL) && (2147483647LL + (long long
)array_size) + (long long )j >= 0LL) && (2147483647LL + (long long )array_size)
+ (long long )temp >= 0LL) && (4294967296LL + (long long )i) + (long long
)j >= 0LL) && (4294967296LL + (long long )i) + (long long )temp >= 0LL) &&
(4294967296LL + (long long )j) + (long long )temp >= 0LL) && (4294967295LL
- (long long )i) + (long long )j >= 0LL) && (4294967295LL - (long long )i)
+ (long long )temp >= 0LL) && (4294967295LL - (long long )j) + (long long
)temp >= 0LL) && (2147483646LL + (long long )array_size) - (long long )i >=
0LL) && (2147483646LL + (long long )array_size) - (long long )j >= 0LL) &&
(2147483646LL + (long long )array_size) - (long long )temp >= 0LL) && (4294967295LL
+ (long long )i) - (long long )j >= 0LL) && (4294967295LL + (long long )i)
- (long long )temp >= 0LL) && (4294967295LL + (long long )j) - (long long
)temp >= 0LL) && (4294967294LL - (long long )i) - (long long )j >= 0LL) &&
(4294967294LL - (long long )i) - (long long )temp >= 0LL) && (4294967294LL
- (long long )j) - (long long )temp >= 0LL)
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i
file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d
line: 554
column: 12
function: SelectionSort
value: 0 <= i
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i
file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d
line: 554
column: 12
function: SelectionSort
value: 0 <= min
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i
file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d
line: 554
column: 12
function: SelectionSort
value: i <= 2147483645
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i
file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d
line: 554
column: 12
function: SelectionSort
value: array_size != 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i
file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d
line: 554
column: 12
function: SelectionSort
value: array_size != 1
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i
file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d
line: 554
column: 12
function: SelectionSort
value: ((((((min <= 2147483646 && ((j != 1 && (((j != 2 && (((j != 3 && (((j
!= 4 && (((j != 5 && (((j != 6 && (((j != 7 && (((j != 8 && (((j != 9 && (((((((11
<= j && (-11LL + (long long )i) + (long long )j >= 0LL) && (-11LL - (long
long )i) + (long long )j >= 0LL) && (11LL + (long long )i) - (long long )j
>= 0LL) && j != 10) && (((((((12 <= array_size && j <= 2147483646) && (-23LL
+ (long long )array_size) + (long long )j >= 0LL) && (-12LL + (long long )array_size)
+ (long long )i >= 0LL) && (-12LL + (long long )array_size) - (long long )i
>= 0LL) && (-1LL + (long long )array_size) - (long long )j >= 0LL) && j !=
0) || ((((11 <= array_size && (-22LL + (long long )array_size) + (long long
)j >= 0LL) && (-11LL + (long long )array_size) + (long long )i >= 0LL) &&
(-11LL + (long long )array_size) - (long long )i >= 0LL) && (long long )array_size
- (long long )j >= 0LL))) || ((((((((((10 <= j && 11 <= array_size) && j <=
2147483646) && (-21LL + (long long )array_size) + (long long )j >= 0LL) &&
(-11LL + (long long )array_size) + (long long )i >= 0LL) && (-10LL + (long
long )i) + (long long )j >= 0LL) && (-10LL - (long long )i) + (long long )j
>= 0LL) && (-11LL + (long long )array_size) - (long long )i >= 0LL) && (-1LL
+ (long long )array_size) - (long long )j >= 0LL) && (10LL + (long long )i)
- (long long )j >= 0LL) && j != 0)) || ((((((((10 <= array_size && 10 <= j)
&& (-20LL + (long long )array_size) + (long long )j >= 0LL) && (-10LL + (long
long )array_size) + (long long )i >= 0LL) && (-10LL + (long long )i) + (long
long )j >= 0LL) && (-10LL - (long long )i) + (long long )j >= 0LL) && (-10LL
+ (long long )array_size) - (long long )i >= 0LL) && (10LL + (long long )i)
- (long long )j >= 0LL) && (long long )array_size - (long long )j >= 0LL)))
|| ((((((((((9 <= j && 10 <= array_size) && j <= 2147483646) && (-19LL + (long
long )array_size) + (long long )j >= 0LL) && (-10LL + (long long )array_size)
+ (long long )i >= 0LL) && (-9LL + (long long )i) + (long long )j >= 0LL)
&& (-9LL - (long long )i) + (long long )j >= 0LL) && (-10LL + (long long )array_size)
- (long long )i >= 0LL) && (-1LL + (long long )array_size) - (long long )j
>= 0LL) && (9LL + (long long )i) - (long long )j >= 0LL) && j != 0)) || ((((((((9
<= array_size && 9 <= j) && (-18LL + (long long )array_size) + (long long
)j >= 0LL) && (-9LL + (long long )array_size) + (long long )i >= 0LL) && (-9LL
+ (long long )i) + (long long )j >= 0LL) && (-9LL - (long long )i) + (long
long )j >= 0LL) && (-9LL + (long long )array_size) - (long long )i >= 0LL)
&& (9LL + (long long )i) - (long long )j >= 0LL) && (long long )array_size
- (long long )j >= 0LL))) || ((((((((((8 <= j && 9 <= array_size) && j <=
2147483646) && (-17LL + (long long )array_size) + (long long )j >= 0LL) &&
(-9LL + (long long )array_size) + (long long )i >= 0LL) && (-8LL + (long long
)i) + (long long )j >= 0LL) && (-8LL - (long long )i) + (long long )j >= 0LL)
&& (-9LL + (long long )array_size) - (long long )i >= 0LL) && (-1LL + (long
long )array_size) - (long long )j >= 0LL) && (8LL + (long long )i) - (long
long )j >= 0LL) && j != 0)) || ((((((((8 <= array_size && 8 <= j) && (-16LL
+ (long long )array_size) + (long long )j >= 0LL) && (-8LL + (long long )array_size)
+ (long long )i >= 0LL) && (-8LL + (long long )i) + (long long )j >= 0LL)
&& (-8LL - (long long )i) + (long long )j >= 0LL) && (-8LL + (long long )array_size)
- (long long )i >= 0LL) && (8LL + (long long )i) - (long long )j >= 0LL) &&
(long long )array_size - (long long )j >= 0LL))) || ((((((((((7 <= j && 8
<= array_size) && j <= 2147483646) && (-15LL + (long long )array_size) + (long
long )j >= 0LL) && (-8LL + (long long )array_size) + (long long )i >= 0LL)
&& (-7LL + (long long )i) + (long long )j >= 0LL) && (-7LL - (long long )i)
+ (long long )j >= 0LL) && (-8LL + (long long )array_size) - (long long )i
>= 0LL) && (-1LL + (long long )array_size) - (long long )j >= 0LL) && (7LL
+ (long long )i) - (long long )j >= 0LL) && j != 0)) || ((((((((7 <= array_size
&& 7 <= j) && (-14LL + (long long )array_size) + (long long )j >= 0LL) &&
(-7LL + (long long )array_size) + (long long )i >= 0LL) && (-7LL + (long long
)i) + (long long )j >= 0LL) && (-7LL - (long long )i) + (long long )j >= 0LL)
&& (-7LL + (long long )array_size) - (long long )i >= 0LL) && (7LL + (long
long )i) - (long long )j >= 0LL) && (long long )array_size - (long long )j
>= 0LL))) || ((((((((((6 <= j && 7 <= array_size) && j <= 2147483646) && (-13LL
+ (long long )array_size) + (long long )j >= 0LL) && (-7LL + (long long )array_size)
+ (long long )i >= 0LL) && (-6LL + (long long )i) + (long long )j >= 0LL)
&& (-6LL - (long long )i) + (long long )j >= 0LL) && (-7LL + (long long )array_size)
- (long long )i >= 0LL) && (-1LL + (long long )array_size) - (long long )j
>= 0LL) && (6LL + (long long )i) - (long long )j >= 0LL) && j != 0)) || ((((((((6
<= array_size && 6 <= j) && (-12LL + (long long )array_size) + (long long
)j >= 0LL) && (-6LL + (long long )array_size) + (long long )i >= 0LL) && (-6LL
+ (long long )i) + (long long )j >= 0LL) && (-6LL - (long long )i) + (long
long )j >= 0LL) && (-6LL + (long long )array_size) - (long long )i >= 0LL)
&& (6LL + (long long )i) - (long long )j >= 0LL) && (long long )array_size
- (long long )j >= 0LL))) || ((((((((((5 <= j && 6 <= array_size) && j <=
2147483646) && (-11LL + (long long )array_size) + (long long )j >= 0LL) &&
(-6LL + (long long )array_size) + (long long )i >= 0LL) && (-5LL + (long long
)i) + (long long )j >= 0LL) && (-5LL - (long long )i) + (long long )j >= 0LL)
&& (-6LL + (long long )array_size) - (long long )i >= 0LL) && (-1LL + (long
long )array_size) - (long long )j >= 0LL) && (5LL + (long long )i) - (long
long )j >= 0LL) && j != 0)) || ((((((((5 <= array_size && 5 <= j) && (-10LL
+ (long long )array_size) + (long long )j >= 0LL) && (-5LL + (long long )array_size)
+ (long long )i >= 0LL) && (-5LL + (long long )i) + (long long )j >= 0LL)
&& (-5LL - (long long )i) + (long long )j >= 0LL) && (-5LL + (long long )array_size)
- (long long )i >= 0LL) && (5LL + (long long )i) - (long long )j >= 0LL) &&
(long long )array_size - (long long )j >= 0LL))) || ((((((((((4 <= j && 5
<= array_size) && j <= 2147483646) && (-9LL + (long long )array_size) + (long
long )j >= 0LL) && (-5LL + (long long )array_size) + (long long )i >= 0LL)
&& (-4LL + (long long )i) + (long long )j >= 0LL) && (-4LL - (long long )i)
+ (long long )j >= 0LL) && (-5LL + (long long )array_size) - (long long )i
>= 0LL) && (-1LL + (long long )array_size) - (long long )j >= 0LL) && (4LL
+ (long long )i) - (long long )j >= 0LL) && j != 0)) || ((((((((4 <= array_size
&& 4 <= j) && (-8LL + (long long )array_size) + (long long )j >= 0LL) && (-4LL
+ (long long )array_size) + (long long )i >= 0LL) && (-4LL + (long long )i)
+ (long long )j >= 0LL) && (-4LL - (long long )i) + (long long )j >= 0LL)
&& (-4LL + (long long )array_size) - (long long )i >= 0LL) && (4LL + (long
long )i) - (long long )j >= 0LL) && (long long )array_size - (long long )j
>= 0LL))) || ((((((((((3 <= j && 4 <= array_size) && j <= 2147483646) && (-7LL
+ (long long )array_size) + (long long )j >= 0LL) && (-4LL + (long long )array_size)
+ (long long )i >= 0LL) && (-3LL + (long long )i) + (long long )j >= 0LL)
&& (-3LL - (long long )i) + (long long )j >= 0LL) && (-4LL + (long long )array_size)
- (long long )i >= 0LL) && (-1LL + (long long )array_size) - (long long )j
>= 0LL) && (3LL + (long long )i) - (long long )j >= 0LL) && j != 0)) || ((((((((3
<= array_size && 3 <= j) && (-6LL + (long long )array_size) + (long long )j
>= 0LL) && (-3LL + (long long )array_size) + (long long )i >= 0LL) && (-3LL
+ (long long )i) + (long long )j >= 0LL) && (-3LL - (long long )i) + (long
long )j >= 0LL) && (-3LL + (long long )array_size) - (long long )i >= 0LL)
&& (3LL + (long long )i) - (long long )j >= 0LL) && (long long )array_size
- (long long )j >= 0LL))) || ((((((((((2 <= j && 3 <= array_size) && j <=
2147483646) && (-5LL + (long long )array_size) + (long long )j >= 0LL) &&
(-3LL + (long long )array_size) + (long long )i >= 0LL) && (-2LL + (long long
)i) + (long long )j >= 0LL) && (-2LL - (long long )i) + (long long )j >= 0LL)
&& (-3LL + (long long )array_size) - (long long )i >= 0LL) && (-1LL + (long
long )array_size) - (long long )j >= 0LL) && (2LL + (long long )i) - (long
long )j >= 0LL) && j != 0)) || ((((((((2 <= array_size && 2 <= j) && (-4LL
+ (long long )array_size) + (long long )j >= 0LL) && (-2LL + (long long )array_size)
+ (long long )i >= 0LL) && (-2LL + (long long )i) + (long long )j >= 0LL)
&& (-2LL - (long long )i) + (long long )j >= 0LL) && (-2LL + (long long )array_size)
- (long long )i >= 0LL) && (2LL + (long long )i) - (long long )j >= 0LL) &&
(long long )array_size - (long long )j >= 0LL))) || ((((((((((1 <= j && 2
<= array_size) && j <= 2147483646) && (-3LL + (long long )array_size) + (long
long )j >= 0LL) && (-2LL + (long long )array_size) + (long long )i >= 0LL)
&& (-1LL + (long long )i) + (long long )j >= 0LL) && (-1LL - (long long )i)
+ (long long )j >= 0LL) && (-2LL + (long long )array_size) - (long long )i
>= 0LL) && (-1LL + (long long )array_size) - (long long )j >= 0LL) && (1LL
+ (long long )i) - (long long )j >= 0LL) && j != 0))) || (((((((((((1 <= j
&& 2 <= array_size) && j <= 2147483646) && min <= 2147483645) && (-3LL + (long
long )array_size) + (long long )j >= 0LL) && (-2LL + (long long )array_size)
+ (long long )i >= 0LL) && (-1LL + (long long )i) + (long long )j >= 0LL)
&& (-1LL - (long long )i) + (long long )j >= 0LL) && (-2LL + (long long )array_size)
- (long long )i >= 0LL) && (-1LL + (long long )array_size) - (long long )j
>= 0LL) && (1LL + (long long )i) - (long long )j >= 0LL) && i == min)) ||
((((((((((((13 <= j && 14 <= array_size) && j <= 2147483646) && (-27LL + (long
long )array_size) + (long long )j >= 0LL) && (-14LL + (long long )array_size)
+ (long long )i >= 0LL) && (-13LL + (long long )i) + (long long )j >= 0LL)
&& (-13LL - (long long )i) + (long long )j >= 0LL) && (-14LL + (long long
)array_size) - (long long )i >= 0LL) && (-1LL + (long long )array_size) -
(long long )j >= 0LL) && j != 0) && j != 1) && j != 2) && j != 3)) || ((((((((2
<= array_size && min <= 2147483645) && (-2LL + (long long )array_size) + (long
long )i >= 0LL) && (2147483646LL + (long long )array_size) + (long long )j
>= 0LL) && (2147483648LL + (long long )i) + (long long )j >= 0LL) && (2147483648LL
- (long long )i) + (long long )j >= 0LL) && (-2LL + (long long )array_size)
- (long long )i >= 0LL) && (2147483646LL + (long long )array_size) - (long
long )j >= 0LL) && i == min)) || ((((((((((13 <= array_size && 13 <= j) &&
(-26LL + (long long )array_size) + (long long )j >= 0LL) && (-13LL + (long
long )array_size) + (long long )i >= 0LL) && (-13LL + (long long )i) + (long
long )j >= 0LL) && (-13LL - (long long )i) + (long long )j >= 0LL) && (-13LL
+ (long long )array_size) - (long long )i >= 0LL) && (long long )array_size
- (long long )j >= 0LL) && j != 1) && j != 2) && j != 3)) || ((((((((((((((((((((((12
<= j && 13 <= array_size) && j <= 2147483646) && min <= 2147483646) && (-25LL
+ (long long )array_size) + (long long )j >= 0LL) && (-13LL + (long long )array_size)
+ (long long )i >= 0LL) && (-12LL + (long long )i) + (long long )j >= 0LL)
&& (-12LL - (long long )i) + (long long )j >= 0LL) && (-13LL + (long long
)array_size) - (long long )i >= 0LL) && (-1LL + (long long )array_size) -
(long long )j >= 0LL) && (12LL + (long long )i) - (long long )j >= 0LL) &&
j != 0) && j != 1) && j != 2) && j != 3) && j != 4) && j != 5) && j != 6)
&& j != 7) && j != 8) && j != 9) && j != 10) && j != 11)) || ((((((((((((((((((((12
<= array_size && 12 <= j) && min <= 2147483646) && (-24LL + (long long )array_size)
+ (long long )j >= 0LL) && (-12LL + (long long )array_size) + (long long )i
>= 0LL) && (-12LL + (long long )i) + (long long )j >= 0LL) && (-12LL - (long
long )i) + (long long )j >= 0LL) && (-12LL + (long long )array_size) - (long
long )i >= 0LL) && (12LL + (long long )i) - (long long )j >= 0LL) && (long
long )array_size - (long long )j >= 0LL) && j != 1) && j != 2) && j != 3)
&& j != 4) && j != 5) && j != 6) && j != 7) && j != 8) && j != 9) && j !=
10) && j != 11)
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
30 |
2023-12-01T05:12:53+01:00 |
|