1cb1945 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T07:38:38Z |
|
084a452 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T17:44:26+01:00 |
|
c949b00 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:36 CET (comp) |
|
cc0b93b |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
7 |
2023-12-02T15:59:13Z |
|
84f0a3b |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Mopsa (v1.0~pre2) |
3 |
2023-11-29T13:14:50Z |
|
1f96fba |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Kojak |
7 |
2023-12-02T22:17:36Z |
|
a1f0385 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
22 |
2023-12-01T01:48:07Z |
|
4d497ff |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-20T03:41:16+01:00 |
c949b00 |
1066a0d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-19T15:16:16+01:00 |
f36b335 |
debf119 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-19T04:35:13+01:00 |
bb36a18 |
b5800cb |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-17T06:04:16+01:00 |
c79fecd |
311cc1a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-04T11:50:09+01:00 |
cc0b93b |
9fb0c60 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-04T01:15:45+01:00 |
5b5b098 |
faebf68 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-03T18:33:55+01:00 |
084a452 |
ebb07ef |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-03T10:00:53+01:00 |
1cb1945 |
806d901 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-03T06:02:08+01:00 |
1f96fba |
44448cb |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-01T03:44:09+01:00 |
a1f0385 |
7b7119c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-01T00:14:03+01:00 |
cc10285 |
f828453 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-11-30T11:27:20+01:00 |
23ecbb2 |
23ecbb2 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-11-30T07:40:49+01:00 |
|
15b1ad4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-11-29T18:24:24+01:00 |
84f0a3b |
727534c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-11-29T08:07:08+01:00 |
acad868 |
5b5b098 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
5 |
2023-12-04T00:04:02+01:00 |
|
c79fecd |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.1 |
5 |
2023-12-17T04:02:29+01:00 |
|
bb36a18 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
5 |
2023-12-18T16:48:11+01:00 |
|
acad868 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
7 |
2023-11-29T01:55:56Z |
|
cc10285 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
2LS |
9 |
2023-11-30T21:32:13+01:00 |
|
0eee70f |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
3 |
2023-12-01T01:59:02Z |
|
3e97e87 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
2LS |
9 |
2023-11-30T22:25:09+01:00 |
|
8ac97fe |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: a0745b0a-bcb9-4f93-b30f-7b3ee0ec2767
creation_time: '2023-11-29T02:55:56+01:00'
producer:
name: Automizer
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3081f57d-78ef-494e-b05f-b8524562c350/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3081f57d-78ef-494e-b05f-b8524562c350/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2.c
: a723a67708085ac2edc65dca820ea0ff5f017c1387423fea83ca87f76f9f53c3
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_3081f57d-78ef-494e-b05f-b8524562c350/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2.c
file_hash: a723a67708085ac2edc65dca820ea0ff5f017c1387423fea83ca87f76f9f53c3
line: 17
column: 0
function: main
value: (((N == i) && (N <= 2147483647)) || ((((N <= 2147483648) && (i <= 2147483646)) && (i <= N)) && (j <= 2147483647)))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3081f57d-78ef-494e-b05f-b8524562c350/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2.c
file_hash: a723a67708085ac2edc65dca820ea0ff5f017c1387423fea83ca87f76f9f53c3
line: 19
column: 0
function: main
value: ((((((N <= 2147483648) && (j <= 2147483648)) && (1 <= i)) && (i <= 2147483646)) && (i <= N)) || ((((1 <= i) && (i <= N)) && (j <= 2147483647)) && (N <= 2147483647)))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-11-29T07:49:34+01:00 |
|
e009af2 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 98690c08-d962-4dcb-a08c-afa45f6d4c80
creation_time: '2023-12-02T23:17:36+01:00'
producer:
name: Kojak
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a6bc94dc-c8a5-4ef5-8663-74443628391c/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a6bc94dc-c8a5-4ef5-8663-74443628391c/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2.c
: a723a67708085ac2edc65dca820ea0ff5f017c1387423fea83ca87f76f9f53c3
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_a6bc94dc-c8a5-4ef5-8663-74443628391c/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2.c
file_hash: a723a67708085ac2edc65dca820ea0ff5f017c1387423fea83ca87f76f9f53c3
line: 17
column: 0
function: main
value: (((N == i) && (N <= 2147483647)) || (((N <= 2147483648) && (i <= 2147483647)) && (1 <= N)))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a6bc94dc-c8a5-4ef5-8663-74443628391c/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2.c
file_hash: a723a67708085ac2edc65dca820ea0ff5f017c1387423fea83ca87f76f9f53c3
line: 19
column: 0
function: main
value: (((((N <= 2147483648) && (j <= 2147483648)) && (1 <= i)) && (i <= 2147483647)) && (1 <= N))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-03T05:40:57+01:00 |
|
4cf7e68 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 4bb3ff6f-d497-4f03-84d0-5e6e6304a017
creation_time: '2023-12-02T16:59:13+01:00'
producer:
name: Taipan
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_34a9a916-5157-43ee-843c-c87c799f2485/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_34a9a916-5157-43ee-843c-c87c799f2485/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2.c
: a723a67708085ac2edc65dca820ea0ff5f017c1387423fea83ca87f76f9f53c3
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_34a9a916-5157-43ee-843c-c87c799f2485/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2.c
file_hash: a723a67708085ac2edc65dca820ea0ff5f017c1387423fea83ca87f76f9f53c3
line: 17
column: 0
function: main
value: (((N == i) && (N <= 2147483647)) || (((N <= 2147483648) && (i <= N)) && (j <= 2147483647)))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_34a9a916-5157-43ee-843c-c87c799f2485/sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2.c
file_hash: a723a67708085ac2edc65dca820ea0ff5f017c1387423fea83ca87f76f9f53c3
line: 19
column: 0
function: main
value: ((((N <= 2147483648) && (j <= 2147483648)) && (1 <= i)) && (i <= N))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-04T11:59:09+01:00 |
|
5fc2e80 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: 2c2a6ff0-2ac3-428b-9e58-f6ed9159906a
creation_time: 2023-12-01T01:48:07Z
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-while2.c'''
task:
input_files:
- ../../sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2.c
input_file_hashes:
../../sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2.c: a723a67708085ac2edc65dca820ea0ff5f017c1387423fea83ca87f76f9f53c3
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-while2.c
file_hash: a723a67708085ac2edc65dca820ea0ff5f017c1387423fea83ca87f76f9f53c3
line: 19
column: 9
function: main
value: 1 <= i
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2.c
file_hash: a723a67708085ac2edc65dca820ea0ff5f017c1387423fea83ca87f76f9f53c3
line: 19
column: 9
function: main
value: (long long )N - (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2.c
file_hash: a723a67708085ac2edc65dca820ea0ff5f017c1387423fea83ca87f76f9f53c3
line: 19
column: 9
function: main
value: i != 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2.c
file_hash: a723a67708085ac2edc65dca820ea0ff5f017c1387423fea83ca87f76f9f53c3
line: 19
column: 9
function: main
value: (((((0 <= j && (-1LL + (long long )i) + (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 && ((j
!= -12 && ((j != -13 && ((j != -14 && ((j != -15 && (((((((j <= 2147483631
&& (-17LL + (long long )N) + (long long )i >= 0LL) && (-16LL + (long long
)N) + (long long )j >= 0LL) && (16LL - (long long )i) + (long long )j >= 0LL)
&& (16LL - (long long )N) + (long long )j >= 0LL) && (-16LL + (long long )N)
- (long long )j >= 0LL) && j != -16) || (((((j <= 2147483632 && (-16LL + (long
long )N) + (long long )i >= 0LL) && (-15LL + (long long )N) + (long long )j
>= 0LL) && (15LL - (long long )i) + (long long )j >= 0LL) && (15LL - (long
long )N) + (long long )j >= 0LL) && (-15LL + (long long )N) - (long long )j
>= 0LL))) || (((((j <= 2147483633 && (-15LL + (long long )N) + (long long
)i >= 0LL) && (-14LL + (long long )N) + (long long )j >= 0LL) && (14LL - (long
long )i) + (long long )j >= 0LL) && (14LL - (long long )N) + (long long )j
>= 0LL) && (-14LL + (long long )N) - (long long )j >= 0LL))) || (((((j <=
2147483634 && (-14LL + (long long )N) + (long long )i >= 0LL) && (-13LL +
(long long )N) + (long long )j >= 0LL) && (13LL - (long long )i) + (long long
)j >= 0LL) && (13LL - (long long )N) + (long long )j >= 0LL) && (-13LL + (long
long )N) - (long long )j >= 0LL))) || (((((j <= 2147483635 && (-13LL + (long
long )N) + (long long )i >= 0LL) && (-12LL + (long long )N) + (long long )j
>= 0LL) && (12LL - (long long )i) + (long long )j >= 0LL) && (12LL - (long
long )N) + (long long )j >= 0LL) && (-12LL + (long long )N) - (long long )j
>= 0LL))) || (((((j <= 2147483636 && (-12LL + (long long )N) + (long long
)i >= 0LL) && (-11LL + (long long )N) + (long long )j >= 0LL) && (11LL - (long
long )i) + (long long )j >= 0LL) && (11LL - (long long )N) + (long long )j
>= 0LL) && (-11LL + (long long )N) - (long long )j >= 0LL))) || (((((j <=
2147483637 && (-11LL + (long long )N) + (long long )i >= 0LL) && (-10LL +
(long long )N) + (long long )j >= 0LL) && (10LL - (long long )i) + (long long
)j >= 0LL) && (10LL - (long long )N) + (long long )j >= 0LL) && (-10LL + (long
long )N) - (long long )j >= 0LL))) || (((((j <= 2147483638 && (-10LL + (long
long )N) + (long long )i >= 0LL) && (-9LL + (long long )N) + (long long )j
>= 0LL) && (9LL - (long long )i) + (long long )j >= 0LL) && (9LL - (long long
)N) + (long long )j >= 0LL) && (-9LL + (long long )N) - (long long )j >= 0LL)))
|| (((((j <= 2147483639 && (-9LL + (long long )N) + (long long )i >= 0LL)
&& (-8LL + (long long )N) + (long long )j >= 0LL) && (8LL - (long long )i)
+ (long long )j >= 0LL) && (8LL - (long long )N) + (long long )j >= 0LL) &&
(-8LL + (long long )N) - (long long )j >= 0LL))) || (((((j <= 2147483640 &&
(-8LL + (long long )N) + (long long )i >= 0LL) && (-7LL + (long long )N) +
(long long )j >= 0LL) && (7LL - (long long )i) + (long long )j >= 0LL) &&
(7LL - (long long )N) + (long long )j >= 0LL) && (-7LL + (long long )N) -
(long long )j >= 0LL)) || (((((((((((((((((((((j <= 2147483622 && (-26LL +
(long long )N) + (long long )i >= 0LL) && (-25LL + (long long )N) + (long
long )j >= 0LL) && (-25LL + (long long )N) - (long long )j >= 0LL) && j !=
-25) && j != -24) && j != -23) && j != -22) && j != -21) && j != -20) && j
!= -19) && j != -18) && j != -17) && j != -16) && j != -15) && j != -14) &&
j != -13) && j != -12) && j != -11) && j != -10) && j != -9) && j != -8)))
|| (((((j <= 2147483641 && (-7LL + (long long )N) + (long long )i >= 0LL)
&& (-6LL + (long long )N) + (long long )j >= 0LL) && (6LL - (long long )i)
+ (long long )j >= 0LL) && (6LL - (long long )N) + (long long )j >= 0LL) &&
(-6LL + (long long )N) - (long long )j >= 0LL)) || (((((((((((((((((((((((j
<= 2147483623 && (-25LL + (long long )N) + (long long )i >= 0LL) && (-24LL
+ (long long )N) + (long long )j >= 0LL) && (24LL - (long long )i) + (long
long )j >= 0LL) && (24LL - (long long )N) + (long long )j >= 0LL) && (-24LL
+ (long long )N) - (long long )j >= 0LL) && j != -24) && j != -23) && j !=
-22) && j != -21) && j != -20) && j != -19) && j != -18) && j != -17) && j
!= -16) && j != -15) && j != -14) && j != -13) && j != -12) && j != -11) &&
j != -10) && j != -9) && j != -8) && j != -7))) || (((((j <= 2147483642 &&
(-6LL + (long long )N) + (long long )i >= 0LL) && (-5LL + (long long )N) +
(long long )j >= 0LL) && (5LL - (long long )i) + (long long )j >= 0LL) &&
(5LL - (long long )N) + (long long )j >= 0LL) && (-5LL + (long long )N) -
(long long )j >= 0LL)) || (((((((((((((((((((((((j <= 2147483624 && (-24LL
+ (long long )N) + (long long )i >= 0LL) && (-23LL + (long long )N) + (long
long )j >= 0LL) && (23LL - (long long )i) + (long long )j >= 0LL) && (23LL
- (long long )N) + (long long )j >= 0LL) && (-23LL + (long long )N) - (long
long )j >= 0LL) && j != -23) && j != -22) && j != -21) && j != -20) && j !=
-19) && j != -18) && j != -17) && j != -16) && j != -15) && j != -14) && j
!= -13) && j != -12) && j != -11) && j != -10) && j != -9) && j != -8) &&
j != -7) && j != -6))) || (((((j <= 2147483643 && (-5LL + (long long )N) +
(long long )i >= 0LL) && (-4LL + (long long )N) + (long long )j >= 0LL) &&
(4LL - (long long )i) + (long long )j >= 0LL) && (4LL - (long long )N) + (long
long )j >= 0LL) && (-4LL + (long long )N) - (long long )j >= 0LL)) || (((((((((((((((((((((((j
<= 2147483625 && (-23LL + (long long )N) + (long long )i >= 0LL) && (-22LL
+ (long long )N) + (long long )j >= 0LL) && (22LL - (long long )i) + (long
long )j >= 0LL) && (22LL - (long long )N) + (long long )j >= 0LL) && (-22LL
+ (long long )N) - (long long )j >= 0LL) && j != -22) && j != -21) && j !=
-20) && j != -19) && j != -18) && j != -17) && j != -16) && j != -15) && j
!= -14) && j != -13) && j != -12) && j != -11) && j != -10) && j != -9) &&
j != -8) && j != -7) && j != -6) && j != -5))) || (((((j <= 2147483644 &&
(-4LL + (long long )N) + (long long )i >= 0LL) && (-3LL + (long long )N) +
(long long )j >= 0LL) && (3LL - (long long )i) + (long long )j >= 0LL) &&
(3LL - (long long )N) + (long long )j >= 0LL) && (-3LL + (long long )N) -
(long long )j >= 0LL)) || (((((((((((((((((((((((j <= 2147483626 && (-22LL
+ (long long )N) + (long long )i >= 0LL) && (-21LL + (long long )N) + (long
long )j >= 0LL) && (21LL - (long long )i) + (long long )j >= 0LL) && (21LL
- (long long )N) + (long long )j >= 0LL) && (-21LL + (long long )N) - (long
long )j >= 0LL) && j != -21) && j != -20) && j != -19) && j != -18) && j !=
-17) && j != -16) && j != -15) && j != -14) && j != -13) && j != -12) && j
!= -11) && j != -10) && j != -9) && j != -8) && j != -7) && j != -6) && j
!= -5) && j != -4))) || (((((j <= 2147483645 && (-3LL + (long long )N) + (long
long )i >= 0LL) && (-2LL + (long long )N) + (long long )j >= 0LL) && (2LL
- (long long )i) + (long long )j >= 0LL) && (2LL - (long long )N) + (long
long )j >= 0LL) && (-2LL + (long long )N) - (long long )j >= 0LL)) || (((((((((((((((((((((((j
<= 2147483627 && (-21LL + (long long )N) + (long long )i >= 0LL) && (-20LL
+ (long long )N) + (long long )j >= 0LL) && (20LL - (long long )i) + (long
long )j >= 0LL) && (20LL - (long long )N) + (long long )j >= 0LL) && (-20LL
+ (long long )N) - (long long )j >= 0LL) && j != -20) && j != -19) && j !=
-18) && j != -17) && j != -16) && j != -15) && j != -14) && j != -13) && j
!= -12) && j != -11) && j != -10) && j != -9) && j != -8) && j != -7) && j
!= -6) && j != -5) && j != -4) && j != -3))) || (((((j <= 2147483646 && (-2LL
+ (long long )N) + (long long )i >= 0LL) && (-1LL + (long long )N) + (long
long )j >= 0LL) && (1LL - (long long )i) + (long long )j >= 0LL) && (1LL -
(long long )N) + (long long )j >= 0LL) && (-1LL + (long long )N) - (long long
)j >= 0LL)) || (((((((((((((((((((((((j <= 2147483628 && (-20LL + (long long
)N) + (long long )i >= 0LL) && (-19LL + (long long )N) + (long long )j >=
0LL) && (19LL - (long long )i) + (long long )j >= 0LL) && (19LL - (long long
)N) + (long long )j >= 0LL) && (-19LL + (long long )N) - (long long )j >=
0LL) && j != -19) && j != -18) && j != -17) && j != -16) && j != -15) && j
!= -14) && j != -13) && j != -12) && j != -11) && j != -10) && j != -9) &&
j != -8) && j != -7) && j != -6) && j != -5) && j != -4) && j != -3) && j
!= -2))) || ((((((((1 <= j && (-2LL + (long long )i) + (long long )j >= 0LL)
&& (-2LL + (long long )N) + (long long )i >= 0LL) && (-2LL + (long long )N)
+ (long long )j >= 0LL) && (0LL - (long long )i) + (long long )j >= 0LL) &&
(0LL - (long long )N) + (long long )j >= 0LL) && (long long )N - (long long
)j >= 0LL) && j == N) && j != 0)) || (((((((((((((((((((((((((0 <= j && j
<= 2147483629) && (-19LL + (long long )N) + (long long )i >= 0LL) && (-18LL
+ (long long )N) + (long long )j >= 0LL) && (-1LL + (long long )i) + (long
long )j >= 0LL) && (18LL - (long long )i) + (long long )j >= 0LL) && (18LL
- (long long )N) + (long long )j >= 0LL) && (-18LL + (long long )N) - (long
long )j >= 0LL) && j != -18) && j != -17) && j != -16) && j != -15) && j !=
-14) && j != -13) && j != -12) && j != -11) && j != -10) && j != -9) && j
!= -8) && j != -7) && j != -6) && j != -5) && j != -4) && j != -3) && j !=
-2) && j != -1)) || ((((((((((((((((((((((((0 <= j && j <= 2147483630) &&
(-18LL + (long long )N) + (long long )i >= 0LL) && (-17LL + (long long )N)
+ (long long )j >= 0LL) && (-1LL + (long long )i) + (long long )j >= 0LL)
&& (17LL - (long long )i) + (long long )j >= 0LL) && (17LL - (long long )N)
+ (long long )j >= 0LL) && (-17LL + (long long )N) - (long long )j >= 0LL)
&& j != -17) && j != -16) && j != -15) && j != -14) && j != -13) && j != -12)
&& j != -11) && j != -10) && j != -9) && j != -8) && j != -7) && j != -6)
&& j != -5) && j != -4) && j != -3) && j != -2) && j != -1)
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2.c
file_hash: a723a67708085ac2edc65dca820ea0ff5f017c1387423fea83ca87f76f9f53c3
line: 17
column: 8
function: main
value: (long long )N - (long long )i >= 0LL
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
22 |
2023-12-01T04:57:39+01:00 |
|