Witness Inspection

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).

This link does not point to a witness, but below is a list of witnesses for the same program.

Available Results for the Program from Witness Store SV-COMP '24

Trying to find witnesses for program (26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67, sv-benchmarks/c/termination-restricted-15/NO_04_false-termination_true-no-overflow.c).

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
Download 8286b65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T07:51:32Z
Download 40e69a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:24:17+01:00
Download 6af4af0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download a9a4fd3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 18 2023-12-02T15:28:30Z
Download 1d1055f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T12:50:46Z
Download 7622fd4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 19 2023-12-03T00:38:53Z
Download 7e858a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 45 2023-12-01T01:57:42Z
Download 61b1f04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-20T03:41:18+01:00 Download 6af4af0
Download 2f8b9fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-12-19T14:36:26+01:00 Download a1e3631
Download 668491e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-12-19T03:59:22+01:00 Download 02fd0d3
Download dee9cda Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-12-17T06:12:08+01:00 Download 9d33edc
Download 2c48e55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-04T11:27:53+01:00 Download a9a4fd3
Download 164c411 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-12-04T01:17:35+01:00 Download 83c573e
Download d879461 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-03T18:30:31+01:00 Download 40e69a5
Download 92b9154 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-03T09:58:58+01:00 Download 8286b65
Download d1e6a55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-03T06:04:04+01:00 Download 7622fd4
Download 3a9a657 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-01T03:38:47+01:00 Download 7e858a9
Download c1905ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-30T23:45:32+01:00 Download 98a48ee
Download b86fd19 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 9 2023-11-30T12:41:03+01:00 Download 28d3e61
Download 28d3e61 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-30T07:32:39+01:00
Download b0d94be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-29T18:26:42+01:00 Download 1d1055f
Download 1204dc5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-29T07:56:49+01:00 Download ea09ca6
Download 83c573e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 8 2023-12-03T18:19:02+01:00
Download 9d33edc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 8 2023-12-17T01:46:44+01:00
Download a1e3631 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 8 2023-12-19T13:50:25+01:00
Download 02fd0d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 8 2023-12-18T23:09:26+01:00
Download ea09ca6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 18 2023-11-29T01:29:13Z
Download 98a48ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 21 2023-11-30T21:26:27+01:00
Download 3b3d56c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness VERIFUZZ 4 2023-12-01T22:24:44Z
Download 35963fa Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.3 8 2023-11-30T08:08:14+01:00
Download 3113fc3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 8 2023-12-03T23:17:34+01:00
Download faa2916 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.1 8 2023-12-17T02:57:29+01:00
Download cb1d9cb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 8 2023-12-18T18:19:58+01:00
Download d822370 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 10 2023-11-29T01:57:03Z
Download 6391f84 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 6 2023-11-30T21:14:10+01:00
Download 77b2a62 Inspect Inspect
Validate
- 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
Download 7977dbf Inspect Inspect
Validate
- 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
Download ad54c84 Inspect Inspect
Validate
- 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
Download 3b664ab Inspect Inspect
Validate
- 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

Available Results for the Program from Witness Store SV-COMP '23

Trying to find witnesses for program (26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67, sv-benchmarks/c/termination-restricted-15/NO_04_false-termination_true-no-overflow.c).

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
Download 7e33011 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T10:32:17Z
Download bc78fad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-11T01:48:01+01:00
Download 6af4af0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T11:01 CET (comp)
Download 398d33d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 18 2022-12-14T08:48:31Z
Download fbfede9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T09:31:49Z
Download 15ab558 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 19 2022-12-15T00:26:06Z
Download 34f0384 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp23-0-g4f5dcf38f) 321 2022-12-10T08:19:40Z
Download 7244463 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T11:32:17+01:00 Download 6af4af0
Download 91ff769 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T10:52:56+01:00 Download 398d33d
Download 7028d5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-29T07:40:07+01:00 Download c7d12e4
Download e9b2782 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T06:24:49+01:00 Download 15ab558
Download 934803c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T03:54:31+01:00 Download fbfede9
Download 8db0c4d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-29T03:07:18+01:00 Download c34df33
Download e17e6b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-29T00:06:50+01:00 Download 58f9b15
Download 11291ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T22:51:48+01:00 Download bc78fad
Download db55b5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-28T18:16:12+01:00 Download d369477
Download 63069f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T17:46:01+01:00 Download 7e33011
Download ffabb48 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-28T10:53:40+01:00 Download cd5c8db
Download 99de6e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 9 2023-01-28T00:50:34+01:00 Download 38a52ca
Download e27ef98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-27T23:11:14+01:00 Download 9593435
Download cd5c8db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2022-12-10T16:51:37+01:00
Download c34df33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 8 2022-12-12T02:33:26+01:00
Download 38a52ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 8 2022-12-25T11:43:25+01:00
Download 58f9b15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 8 2022-12-11T04:17:30+01:00
Download d369477 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 8 2022-12-10T00:32:39+01:00
Download c7d12e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 19 2022-12-13T14:42:08Z
Download 9593435 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 21 2022-12-07T23:50:14+01:00
Download 899d34a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.2 8 2022-12-10T17:52:03+01:00
Download eedb94d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 8 2022-12-12T01:30:19+01:00
Download a2f42ed Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.1 8 2022-12-25T13:10:03+01:00
Download aa61a70 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 8 2022-12-10T03:12:24+01:00
Download 3339571 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 10 2022-12-13T11:36:49Z
Download 5c1e45b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 6 2022-12-08T00:01:39+01:00

Available Results for the Program from Witness Store SV-COMP '22

Trying to find witnesses for program (26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67, sv-benchmarks/c/termination-restricted-15/NO_04_false-termination_true-no-overflow.c).

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
Download 65fec39 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.1 8 2021-12-05T18:42:36+01:00
Download 0f7757d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0 8 2021-12-10T18:38:28+01:00
Download 5691ca8 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 8 2021-12-08T19:10:59+01:00
Download 0995379 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 8 2021-12-09T14:15:40+01:00
Download ce2f2cb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 10 2021-12-06T23:24:06Z
Download e0e434d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness AProVE 8 2021-12-05T12:23:06Z
Download 03d5841 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 6 2021-12-05T23:24:53+01:00

Available Results for the Program from Witness Store SV-COMP '21

Trying to find witnesses for program (26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67, sv-benchmarks/c/termination-restricted-15/NO_04_false-termination_true-no-overflow.c).

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
Download 9568ac5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0 8 2020-12-05T16:46:32+01:00
Download 786f716 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 8 2020-12-08T02:41:41+01:00

Available Results for the Program from Witness Store SV-COMP '20

Trying to find witnesses for program (26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67, sv-benchmarks/c/termination-restricted-15/NO_04_false-termination_true-no-overflow.c).

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
Download 915e712 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 8 2019-11-30T06:01:59+01:00
Download c402afa Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 8 2019-12-01T02:03:16+01:00

Available Results for the Program from Witness Store SV-COMP '19

Trying to find witnesses for program (26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67, sv-benchmarks/c/termination-restricted-15/NO_04_false-termination_true-no-overflow.c).

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
Download 9a75dde Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 8 2018-12-07T01:26:29+01:00
Download 8f1c3cb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-09T20:34:09+01:00
Download 924fab1 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-06T09:42:25+01:00
Download 81a8073 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-05T17:19:26+01:00
Download cedee0b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 8 2018-12-05T09:27:26+01:00

Available Results for the Program from Witness Store SV-COMP '18

Trying to find witnesses for program (26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67, sv-benchmarks/c/termination-restricted-15/NO_04_false-termination_true-no-overflow.c).

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
Download a47486f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 40 2017-12-01T18:39 CET (sv-comp)
Download 69a92ed Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T12:36:06+01:00
Download f874026 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 10 2017-12-03T11:16Z
Download eea19b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 7 2017-12-01T12:04 CET (sv-comp)

Available Results for the Program from Witness Store SV-COMP '17

Trying to find witnesses for program (26441cee42562e2fd703b97b1a86d2baa847af9810285d31267fccda11d2ea67, sv-benchmarks/c/termination-restricted-15/NO_04_false-termination_true-no-overflow.c).

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