A description of this web service can be found in the CAV paper "Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses" (more material).
Found 39 witnesses for program sv-benchmarks/c/termination-restricted-15/NO_04_false-termination_true-no-overflow.c, 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
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 |
Found 33 witnesses for program sv-benchmarks/c/termination-restricted-15/NO_04_false-termination_true-no-overflow.c, 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7e33011 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T10:32:17Z | ||
bc78fad | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-11T01:48:01+01:00 | ||
6af4af0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2022-12-12T11:01 CET (comp) | ||
398d33d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 18 | 2022-12-14T08:48:31Z | ||
fbfede9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2022-12-11T09:31:49Z | ||
15ab558 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 19 | 2022-12-15T00:26:06Z | ||
34f0384 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp23-0-g4f5dcf38f) | 321 | 2022-12-10T08:19:40Z | ||
7244463 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T11:32:17+01:00 | 6af4af0 | |
91ff769 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T10:52:56+01:00 | 398d33d | |
7028d5f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-29T07:40:07+01:00 | c7d12e4 | |
e9b2782 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T06:24:49+01:00 | 15ab558 | |
934803c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T03:54:31+01:00 | fbfede9 | |
8db0c4d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-29T03:07:18+01:00 | c34df33 | |
e17e6b5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-29T00:06:50+01:00 | 58f9b15 | |
11291ef | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T22:51:48+01:00 | bc78fad | |
db55b5b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-28T18:16:12+01:00 | d369477 | |
63069f9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T17:46:01+01:00 | 7e33011 | |
ffabb48 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-28T10:53:40+01:00 | cd5c8db | |
99de6e8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-28T00:50:34+01:00 | 38a52ca | |
e27ef98 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-27T23:11:14+01:00 | 9593435 | |
cd5c8db | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2022-12-10T16:51:37+01:00 | ||
c34df33 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 8 | 2022-12-12T02:33:26+01:00 | ||
38a52ca | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 8 | 2022-12-25T11:43:25+01:00 | ||
58f9b15 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 8 | 2022-12-11T04:17:30+01:00 | ||
d369477 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 8 | 2022-12-10T00:32:39+01:00 | ||
c7d12e4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 19 | 2022-12-13T14:42:08Z | ||
9593435 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | 2LS | 21 | 2022-12-07T23:50:14+01:00 | ||
899d34a | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 2.2 | 8 | 2022-12-10T17:52:03+01:00 | ||
eedb94d | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 8 | 2022-12-12T01:30:19+01:00 | ||
a2f42ed | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 2.1 | 8 | 2022-12-25T13:10:03+01:00 | ||
aa61a70 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 8 | 2022-12-10T03:12:24+01:00 | ||
3339571 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 10 | 2022-12-13T11:36:49Z | ||
5c1e45b | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 6 | 2022-12-08T00:01:39+01:00 |
Found 7 witnesses for program sv-benchmarks/c/termination-restricted-15/NO_04_false-termination_true-no-overflow.c, 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
65fec39 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 2.1 | 8 | 2021-12-05T18:42:36+01:00 | ||
0f7757d | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 2.0 | 8 | 2021-12-10T18:38:28+01:00 | ||
5691ca8 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 8 | 2021-12-08T19:10:59+01:00 | ||
0995379 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 8 | 2021-12-09T14:15:40+01:00 | ||
ce2f2cb | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 10 | 2021-12-06T23:24:06Z | ||
e0e434d | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | AProVE | 8 | 2021-12-05T12:23:06Z | ||
03d5841 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 6 | 2021-12-05T23:24:53+01:00 |
Found 2 witnesses for program sv-benchmarks/c/termination-restricted-15/NO_04_false-termination_true-no-overflow.c, 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9568ac5 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 2.0 | 8 | 2020-12-05T16:46:32+01:00 | ||
786f716 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 8 | 2020-12-08T02:41:41+01:00 |
Found 2 witnesses for program sv-benchmarks/c/termination-restricted-15/NO_04_false-termination_true-no-overflow.c, 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
915e712 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.9 | 8 | 2019-11-30T06:01:59+01:00 | ||
c402afa | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 8 | 2019-12-01T02:03:16+01:00 |
Found 5 witnesses for program sv-benchmarks/c/termination-restricted-15/NO_04_false-termination_true-no-overflow.c, 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9a75dde | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 8 | 2018-12-07T01:26:29+01:00 | ||
8f1c3cb | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-09T20:34:09+01:00 | ||
924fab1 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T09:42:25+01:00 | ||
81a8073 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-05T17:19:26+01:00 | ||
cedee0b | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-05T09:27:26+01:00 |
Found 4 witnesses for program sv-benchmarks/c/termination-restricted-15/NO_04_false-termination_true-no-overflow.c, 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a47486f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 40 | 2017-12-01T18:39 CET (sv-comp) | ||
69a92ed | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-12-01T12:36:06+01:00 | ||
f874026 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 10 | 2017-12-03T11:16Z | ||
eea19b6 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 7 | 2017-12-01T12:04 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/NO_04_false-termination_true-no-overflow.c, 26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |