8286b65 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T07:51:32Z |
|
40e69a5 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T17:24:17+01:00 |
|
6af4af0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:37 CET (comp) |
|
a9a4fd3 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
18 |
2023-12-02T15:28:30Z |
|
1d1055f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Mopsa (v1.0~pre2) |
3 |
2023-11-29T12:50:46Z |
|
7622fd4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Kojak |
19 |
2023-12-03T00:38:53Z |
|
7e858a9 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
45 |
2023-12-01T01:57:42Z |
|
61b1f04 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-20T03:41:18+01:00 |
6af4af0 |
2f8b9fe |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
9 |
2023-12-19T14:36:26+01:00 |
a1e3631 |
668491e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
9 |
2023-12-19T03:59:22+01:00 |
02fd0d3 |
dee9cda |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
9 |
2023-12-17T06:12:08+01:00 |
9d33edc |
2c48e55 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-04T11:27:53+01:00 |
a9a4fd3 |
164c411 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
9 |
2023-12-04T01:17:35+01:00 |
83c573e |
d879461 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-03T18:30:31+01:00 |
40e69a5 |
92b9154 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-03T09:58:58+01:00 |
8286b65 |
d1e6a55 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-03T06:04:04+01:00 |
7622fd4 |
3a9a657 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-01T03:38:47+01:00 |
7e858a9 |
c1905ad |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-30T23:45:32+01:00 |
98a48ee |
b86fd19 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
9 |
2023-11-30T12:41:03+01:00 |
28d3e61 |
28d3e61 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-30T07:32:39+01:00 |
|
b0d94be |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-29T18:26:42+01:00 |
1d1055f |
1204dc5 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-29T07:56:49+01:00 |
ea09ca6 |
83c573e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
8 |
2023-12-03T18:19:02+01:00 |
|
9d33edc |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.1 |
8 |
2023-12-17T01:46:44+01:00 |
|
a1e3631 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0 |
8 |
2023-12-19T13:50:25+01:00 |
|
02fd0d3 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
8 |
2023-12-18T23:09:26+01:00 |
|
ea09ca6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
18 |
2023-11-29T01:29:13Z |
|
98a48ee |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
2LS |
21 |
2023-11-30T21:26:27+01:00 |
|
3b3d56c |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
VERIFUZZ |
4 |
2023-12-01T22:24:44Z |
|
35963fa |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.3 |
8 |
2023-11-30T08:08:14+01:00 |
|
3113fc3 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
8 |
2023-12-03T23:17:34+01:00 |
|
faa2916 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.1 |
8 |
2023-12-17T02:57:29+01:00 |
|
cb1d9cb |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
8 |
2023-12-18T18:19:58+01:00 |
|
d822370 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
Automizer |
10 |
2023-11-29T01:57:03Z |
|
6391f84 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
2LS |
6 |
2023-11-30T21:14:10+01:00 |
|
77b2a62 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 9f006736-14e8-40d4-a8c7-d51646cd2258
creation_time: '2023-12-03T01:38:54+01:00'
producer:
name: Kojak
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d8207616-cb9f-40f3-985f-c94a1a7cfc42/sv-benchmarks/c/termination-restricted-15/NO_04.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d8207616-cb9f-40f3-985f-c94a1a7cfc42/sv-benchmarks/c/termination-restricted-15/NO_04.c
: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
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_d8207616-cb9f-40f3-985f-c94a1a7cfc42/sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 0
function: main
value: ((i <= 0) && (0 <= i))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d8207616-cb9f-40f3-985f-c94a1a7cfc42/sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 0
function: main
value: (((((0 <= (i + j)) && (i <= 0)) && ((i + j) <= 0)) && (0 <= i)) && ((2 + j) <= a))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d8207616-cb9f-40f3-985f-c94a1a7cfc42/sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 0
function: main
value: (((((((i + j) + k) <= 3) && (0 <= (i + j))) && (i <= 0)) && (0 <= i)) && (3 <= k))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d8207616-cb9f-40f3-985f-c94a1a7cfc42/sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 0
function: main
value: (((((((((0 <= ((i + j) + k)) && (0 <= (i + j))) && ((((i + j) + k) + l) <= 3)) && (0 <= j)) && ((i + j) <= 0)) && (l <= 0)) && (0 <= l)) && ((l + 4) <= b)) && (j <= 0))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d8207616-cb9f-40f3-985f-c94a1a7cfc42/sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 0
function: main
value: (((((0 <= m) && (m < 1000)) && (0 <= l)) || (((1000 <= m) && (m <= 1003)) && (0 <= l))) || (((1003 < m) && (0 <= l)) && (m <= 2147483647)))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
12 |
2023-12-03T05:33:51+01:00 |
|
7977dbf |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 772e6bb2-e187-493d-85cf-e354722cd618
creation_time: '2023-12-02T16:28:31+01:00'
producer:
name: Taipan
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_100414da-9c08-4009-9ac5-ac44e7f88483/sv-benchmarks/c/termination-restricted-15/NO_04.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_100414da-9c08-4009-9ac5-ac44e7f88483/sv-benchmarks/c/termination-restricted-15/NO_04.c
: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
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_100414da-9c08-4009-9ac5-ac44e7f88483/sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 0
function: main
value: ((i == 0) || ((0 < (j + 1)) && (0 <= i)))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_100414da-9c08-4009-9ac5-ac44e7f88483/sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 0
function: main
value: (((i <= 99) && (0 <= i)) && (j == 0))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_100414da-9c08-4009-9ac5-ac44e7f88483/sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 0
function: main
value: ((((k <= 102) && (0 <= i)) && (j == 0)) && ((3 + i) <= k))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_100414da-9c08-4009-9ac5-ac44e7f88483/sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 0
function: main
value: ((((((l == 0) && (k <= 102)) && (0 <= i)) && (7 <= b)) && (j == 0)) && ((3 + i) <= k))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_100414da-9c08-4009-9ac5-ac44e7f88483/sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 0
function: main
value: (((((((((i + j) <= 99) && (0 <= ((i + j) + k))) && (0 <= m)) && (0 <= j)) && ((((i + j) + k) + l) <= 201)) && (0 <= i)) && (m <= 1201)) && (0 <= l))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
12 |
2023-12-04T11:54:23+01:00 |
|
ad54c84 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 10886c7a-c6ad-4e0e-8394-b5acc5364382
creation_time: '2023-11-29T02:29:13+01:00'
producer:
name: Automizer
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_656de687-312f-4804-bb60-496619bf7d12/sv-benchmarks/c/termination-restricted-15/NO_04.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_656de687-312f-4804-bb60-496619bf7d12/sv-benchmarks/c/termination-restricted-15/NO_04.c
: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
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_656de687-312f-4804-bb60-496619bf7d12/sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 0
function: main
value: ((i == 0) || ((0 < (j + 1)) && (0 <= i)))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_656de687-312f-4804-bb60-496619bf7d12/sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 0
function: main
value: (((i <= 99) && (0 <= i)) && (j == 0))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_656de687-312f-4804-bb60-496619bf7d12/sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 0
function: main
value: ((((k <= 102) && (0 <= i)) && (j == 0)) && ((3 + i) <= k))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_656de687-312f-4804-bb60-496619bf7d12/sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 0
function: main
value: ((((((l == 0) && (k <= 102)) && (0 <= i)) && (7 <= b)) && (j == 0)) && ((3 + i) <= k))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_656de687-312f-4804-bb60-496619bf7d12/sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 0
function: main
value: (((((((((i + j) <= 99) && (0 <= ((i + j) + k))) && (0 <= m)) && (0 <= j)) && ((((i + j) + k) + l) <= 201)) && (0 <= i)) && (m <= 1201)) && (0 <= l))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
12 |
2023-11-29T07:43:42+01:00 |
|
3b664ab |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: eedf908e-5459-4410-af84-fae82ff0188f
creation_time: 2023-12-01T01:57: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-restricted-15/NO_04.c'''
task:
input_files:
- ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
input_file_hashes:
../../sv-benchmarks/c/termination-restricted-15/NO_04.c: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
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/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (-2LL + (long long )a) + (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (-2LL + (long long )a) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483646LL + (long long )a) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483646LL + (long long )a) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483646LL + (long long )a) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483646LL + (long long )a) + (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483648LL + (long long )i) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483648LL + (long long )i) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483648LL + (long long )i) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483648LL + (long long )j) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483648LL + (long long )j) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483648LL + (long long )j) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483648LL + (long long )b) + (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483648LL + (long long )b) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967296LL + (long long )k) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967296LL + (long long )k) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967296LL + (long long )l) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967296LL + (long long )b) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967296LL + (long long )b) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967296LL + (long long )b) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (0LL - (long long )i) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2LL - (long long )a) + (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2LL - (long long )a) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483647LL - (long long )b) + (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483647LL - (long long )b) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483648LL - (long long )i) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483648LL - (long long )i) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483648LL - (long long )i) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483648LL - (long long )j) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483648LL - (long long )j) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483648LL - (long long )j) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483650LL - (long long )a) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483650LL - (long long )a) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483650LL - (long long )a) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483650LL - (long long )a) + (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967295LL - (long long )k) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967295LL - (long long )k) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967295LL - (long long )l) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967295LL - (long long )b) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967295LL - (long long )b) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967295LL - (long long )b) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (long long )i + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (-2LL + (long long )a) - (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (-2LL + (long long )a) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483645LL + (long long )a) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483645LL + (long long )a) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483645LL + (long long )a) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483645LL + (long long )a) - (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483647LL + (long long )i) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483647LL + (long long )i) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483647LL + (long long )i) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483647LL + (long long )j) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483647LL + (long long )j) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483647LL + (long long )j) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483648LL + (long long )b) - (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483648LL + (long long )b) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967295LL + (long long )k) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967295LL + (long long )k) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967295LL + (long long )l) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967295LL + (long long )b) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967295LL + (long long )b) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967295LL + (long long )b) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (0LL - (long long )i) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2LL - (long long )a) - (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2LL - (long long )a) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483647LL - (long long )i) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483647LL - (long long )i) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483647LL - (long long )i) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483647LL - (long long )j) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483647LL - (long long )j) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483647LL - (long long )j) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483647LL - (long long )b) - (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483647LL - (long long )b) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483649LL - (long long )a) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483649LL - (long long )a) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483649LL - (long long )a) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (2147483649LL - (long long )a) - (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967294LL - (long long )k) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967294LL - (long long )k) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967294LL - (long long )l) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967294LL - (long long )b) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967294LL - (long long )b) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (4294967294LL - (long long )b) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: (long long )i - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: 0 == i
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: 0 == j
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: i == 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: i == j
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: j == 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 18
column: 15
function: main
value: a == 2
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (-5LL + (long long )a) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (-3LL + (long long )i) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (-3LL + (long long )j) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (-2LL + (long long )a) + (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (-2LL + (long long )a) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483645LL + (long long )k) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483645LL + (long long )k) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483645LL + (long long )b) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483646LL + (long long )a) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483646LL + (long long )a) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483646LL + (long long )a) + (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483648LL + (long long )i) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483648LL + (long long )i) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483648LL + (long long )j) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483648LL + (long long )j) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483648LL + (long long )b) + (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483648LL + (long long )b) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (4294967296LL + (long long )l) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (4294967296LL + (long long )b) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (4294967296LL + (long long )b) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (-3LL - (long long )i) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (-3LL - (long long )j) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (-1LL - (long long )a) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (0LL - (long long )i) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2LL - (long long )a) + (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2LL - (long long )a) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483644LL - (long long )b) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483647LL - (long long )b) + (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483647LL - (long long )b) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483648LL - (long long )i) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483648LL - (long long )i) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483648LL - (long long )j) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483648LL - (long long )j) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483650LL - (long long )a) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483650LL - (long long )a) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483650LL - (long long )a) + (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483651LL - (long long )k) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483651LL - (long long )k) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (4294967295LL - (long long )l) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (4294967295LL - (long long )b) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (4294967295LL - (long long )b) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (long long )i + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (-2LL + (long long )a) - (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (-2LL + (long long )a) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (1LL + (long long )a) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (3LL + (long long )i) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (3LL + (long long )j) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483644LL + (long long )k) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483644LL + (long long )k) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483645LL + (long long )a) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483645LL + (long long )a) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483645LL + (long long )a) - (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483647LL + (long long )i) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483647LL + (long long )i) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483647LL + (long long )j) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483647LL + (long long )j) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483648LL + (long long )b) - (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483648LL + (long long )b) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483651LL + (long long )b) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (4294967295LL + (long long )l) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (4294967295LL + (long long )b) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (4294967295LL + (long long )b) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (0LL - (long long )i) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2LL - (long long )a) - (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2LL - (long long )a) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (3LL - (long long )i) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (3LL - (long long )j) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (5LL - (long long )a) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483647LL - (long long )i) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483647LL - (long long )i) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483647LL - (long long )j) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483647LL - (long long )j) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483647LL - (long long )b) - (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483647LL - (long long )b) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483649LL - (long long )a) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483649LL - (long long )a) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483649LL - (long long )a) - (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483650LL - (long long )k) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483650LL - (long long )k) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (2147483650LL - (long long )b) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (4294967294LL - (long long )l) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (4294967294LL - (long long )b) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (4294967294LL - (long long )b) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: (long long )i - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: 0 == i
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: 0 == j
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: i == 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: i == j
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: j == 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: k == 3
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 20
column: 19
function: main
value: a == 2
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-10LL + (long long )b) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-9LL + (long long )a) + (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-7LL + (long long )b) + (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-7LL + (long long )b) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-7LL + (long long )b) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-5LL + (long long )a) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-3LL + (long long )i) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-3LL + (long long )j) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-3LL + (long long )k) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-2LL + (long long )a) + (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-2LL + (long long )a) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-2LL + (long long )a) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483641LL + (long long )b) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483645LL + (long long )k) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483646LL + (long long )a) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483648LL + (long long )i) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483648LL + (long long )j) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483648LL + (long long )l) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-5LL - (long long )a) + (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-3LL - (long long )i) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-3LL - (long long )j) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-1LL - (long long )a) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (0LL - (long long )i) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (0LL - (long long )i) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (0LL - (long long )j) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2LL - (long long )a) + (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2LL - (long long )a) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2LL - (long long )a) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (3LL - (long long )k) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (4LL - (long long )b) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (7LL - (long long )b) + (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (7LL - (long long )b) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (7LL - (long long )b) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483648LL - (long long )i) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483648LL - (long long )j) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483648LL - (long long )l) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483650LL - (long long )a) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483651LL - (long long )k) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483655LL - (long long )b) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (long long )i + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (long long )i + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (long long )j + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-7LL + (long long )b) - (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-7LL + (long long )b) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-7LL + (long long )b) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-4LL + (long long )b) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-3LL + (long long )k) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-2LL + (long long )a) - (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-2LL + (long long )a) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (-2LL + (long long )a) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (1LL + (long long )a) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (3LL + (long long )i) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (3LL + (long long )j) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (5LL + (long long )a) - (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483640LL + (long long )b) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483644LL + (long long )k) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483645LL + (long long )a) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483647LL + (long long )i) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483647LL + (long long )j) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483647LL + (long long )l) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (0LL - (long long )i) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (0LL - (long long )i) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (0LL - (long long )j) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2LL - (long long )a) - (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2LL - (long long )a) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2LL - (long long )a) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (3LL - (long long )i) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (3LL - (long long )j) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (3LL - (long long )k) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (5LL - (long long )a) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (7LL - (long long )b) - (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (7LL - (long long )b) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (7LL - (long long )b) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (9LL - (long long )a) - (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (10LL - (long long )b) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483647LL - (long long )i) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483647LL - (long long )j) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483647LL - (long long )l) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483649LL - (long long )a) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483650LL - (long long )k) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (2147483654LL - (long long )b) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (long long )i - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (long long )i - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: (long long )j - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: 0 == i
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: 0 == j
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: 0 == l
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: i == 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: i == j
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: i == l
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: j == 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: j == l
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: k == 3
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: l == 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: a == 2
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 23
column: 23
function: main
value: b == 7
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483648LL + (long long )i) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483648LL + (long long )i) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483648LL + (long long )i) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483648LL + (long long )i) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483648LL + (long long )a) + (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483648LL + (long long )b) + (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967296LL + (long long )j) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967296LL + (long long )j) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967296LL + (long long )j) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967296LL + (long long )k) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967296LL + (long long )k) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967296LL + (long long )l) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967296LL + (long long )a) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967296LL + (long long )a) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967296LL + (long long )a) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967296LL + (long long )a) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967296LL + (long long )a) + (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967296LL + (long long )b) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967296LL + (long long )b) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967296LL + (long long )b) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967296LL + (long long )b) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483647LL - (long long )a) + (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483647LL - (long long )b) + (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483648LL - (long long )i) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483648LL - (long long )i) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483648LL - (long long )i) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483648LL - (long long )i) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL - (long long )j) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL - (long long )j) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL - (long long )j) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL - (long long )k) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL - (long long )k) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL - (long long )l) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL - (long long )a) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL - (long long )a) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL - (long long )a) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL - (long long )a) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL - (long long )a) + (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL - (long long )b) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL - (long long )b) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL - (long long )b) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL - (long long )b) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483647LL + (long long )i) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483647LL + (long long )i) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483647LL + (long long )i) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483647LL + (long long )i) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483648LL + (long long )a) - (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483648LL + (long long )b) - (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL + (long long )j) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL + (long long )j) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL + (long long )j) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL + (long long )k) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL + (long long )k) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL + (long long )l) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL + (long long )a) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL + (long long )a) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL + (long long )a) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL + (long long )a) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL + (long long )a) - (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL + (long long )b) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL + (long long )b) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL + (long long )b) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967295LL + (long long )b) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483647LL - (long long )i) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483647LL - (long long )i) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483647LL - (long long )i) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483647LL - (long long )i) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483647LL - (long long )a) - (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (2147483647LL - (long long )b) - (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967294LL - (long long )j) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967294LL - (long long )j) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967294LL - (long long )j) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967294LL - (long long )k) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967294LL - (long long )k) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967294LL - (long long )l) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967294LL - (long long )a) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967294LL - (long long )a) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967294LL - (long long )a) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967294LL - (long long )a) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967294LL - (long long )a) - (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967294LL - (long long )b) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967294LL - (long long )b) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967294LL - (long long )b) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: (4294967294LL - (long long )b) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: 0 == i
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 15
column: 11
function: main
value: i == 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-1010LL + (long long )b) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-1006LL + (long long )k) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-1005LL + (long long )a) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-1003LL + (long long )i) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-1003LL + (long long )j) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-1003LL + (long long )l) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-10LL + (long long )b) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-9LL + (long long )a) + (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-7LL + (long long )b) + (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-7LL + (long long )b) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-7LL + (long long )b) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-5LL + (long long )a) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-3LL + (long long )i) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-3LL + (long long )j) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-3LL + (long long )k) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-2LL + (long long )a) + (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-2LL + (long long )a) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-2LL + (long long )a) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-1003LL - (long long )i) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-1003LL - (long long )j) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-1003LL - (long long )l) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-1001LL - (long long )a) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-1000LL - (long long )k) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-996LL - (long long )b) + (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-5LL - (long long )a) + (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-3LL - (long long )i) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-3LL - (long long )j) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-1LL - (long long )a) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (0LL - (long long )i) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (0LL - (long long )i) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (0LL - (long long )j) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (2LL - (long long )a) + (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (2LL - (long long )a) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (2LL - (long long )a) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (3LL - (long long )k) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (4LL - (long long )b) + (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (7LL - (long long )b) + (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (7LL - (long long )b) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (7LL - (long long )b) + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (long long )i + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (long long )i + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (long long )j + (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-7LL + (long long )b) - (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-7LL + (long long )b) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-7LL + (long long )b) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-4LL + (long long )b) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-3LL + (long long )k) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-2LL + (long long )a) - (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-2LL + (long long )a) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (-2LL + (long long )a) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (1LL + (long long )a) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (3LL + (long long )i) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (3LL + (long long )j) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (5LL + (long long )a) - (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (996LL + (long long )b) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (1000LL + (long long )k) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (1001LL + (long long )a) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (1003LL + (long long )i) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (1003LL + (long long )j) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (1003LL + (long long )l) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (0LL - (long long )i) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (0LL - (long long )i) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (0LL - (long long )j) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (2LL - (long long )a) - (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (2LL - (long long )a) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (2LL - (long long )a) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (3LL - (long long )i) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (3LL - (long long )j) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (3LL - (long long )k) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (5LL - (long long )a) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (7LL - (long long )b) - (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (7LL - (long long )b) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (7LL - (long long )b) - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (9LL - (long long )a) - (long long )b >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (10LL - (long long )b) - (long long )k >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (1003LL - (long long )i) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (1003LL - (long long )j) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (1003LL - (long long )l) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (1005LL - (long long )a) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (1006LL - (long long )k) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (1010LL - (long long )b) - (long long )m >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (long long )i - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (long long )i - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: (long long )j - (long long )l >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: 0 == i
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: 0 == j
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: 0 == l
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: i == 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: i == j
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: i == l
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: j == 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: j == l
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: k == 3
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: l == 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: m == 1003
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: a == 2
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/NO_04.c
file_hash: 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
line: 25
column: 27
function: main
value: b == 7
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
177 |
2023-12-01T04:18:11+01:00 |
|