diff --git a/benchmarks/MBPP/verified/task_id_105.rs b/benchmarks/MBPP/verified/task_id_105.rs index 128cf9ea..77f3ec31 100644 --- a/benchmarks/MBPP/verified/task_id_105.rs +++ b/benchmarks/MBPP/verified/task_id_105.rs @@ -37,6 +37,8 @@ fn count_true(arr: &Vec) -> (count: u64) 0 <= index <= arr.len(), 0 <= counter <= index, count_boolean(arr@.subrange(0, index as int)) == counter, + decreases + arr.len() - index, { if (arr[index]) { counter += 1; diff --git a/benchmarks/MBPP/verified/task_id_113.rs b/benchmarks/MBPP/verified/task_id_113.rs index fda70b04..66d164fa 100644 --- a/benchmarks/MBPP/verified/task_id_113.rs +++ b/benchmarks/MBPP/verified/task_id_113.rs @@ -30,6 +30,8 @@ fn is_integer(text: &Vec) -> (result: bool) invariant 0 <= index <= text.len(), forall|i: int| 0 <= i < index ==> (#[trigger] is_digit_sepc(text[i])), + decreases + text.len() - index, { if (!is_digit(text[index])) { return false; diff --git a/benchmarks/MBPP/verified/task_id_133.rs b/benchmarks/MBPP/verified/task_id_133.rs index 782bf91a..769607fd 100644 --- a/benchmarks/MBPP/verified/task_id_133.rs +++ b/benchmarks/MBPP/verified/task_id_133.rs @@ -42,6 +42,8 @@ fn sum_negatives(arr: &Vec) -> (sum_neg: i128) #[trigger] arr@.subrange(0, j), )) <= 0), sum_negative_to(arr@.subrange(0, index as int)) == sum_neg, + decreases + arr.len() - index, { if (arr[index] < 0) { sum_neg = sum_neg + (arr[index] as i128); diff --git a/benchmarks/MBPP/verified/task_id_142.rs b/benchmarks/MBPP/verified/task_id_142.rs index 2cf2a05f..da9d5187 100644 --- a/benchmarks/MBPP/verified/task_id_142.rs +++ b/benchmarks/MBPP/verified/task_id_142.rs @@ -65,6 +65,8 @@ fn count_identical_position(arr1: &Vec, arr2: &Vec, arr3: &Vec) - arr2@.subrange(0, index as int), arr3@.subrange(0, index as int), ) == count, + decreases + arr1.len() - index, { if arr1[index] == arr2[index] && arr2[index] == arr3[index] { count += 1; diff --git a/benchmarks/MBPP/verified/task_id_145.rs b/benchmarks/MBPP/verified/task_id_145.rs index 47c499af..3d3674f4 100644 --- a/benchmarks/MBPP/verified/task_id_145.rs +++ b/benchmarks/MBPP/verified/task_id_145.rs @@ -28,6 +28,8 @@ fn max_difference(arr: &Vec) -> (diff: i32) min_val <= max_val, forall|i: int| 0 <= i < arr.len() ==> i32::MIN / 2 < #[trigger] arr[i] < i32::MAX / 2, forall|k: int| 0 <= k < index ==> min_val <= arr[k] && arr[k] <= max_val, + decreases + arr.len() - index, { if (arr[index] < min_val) { min_val = arr[index]; diff --git a/benchmarks/MBPP/verified/task_id_161.rs b/benchmarks/MBPP/verified/task_id_161.rs index 5a989ca7..95bd6bdb 100644 --- a/benchmarks/MBPP/verified/task_id_161.rs +++ b/benchmarks/MBPP/verified/task_id_161.rs @@ -36,6 +36,9 @@ fn contains(str: &Vec, key: i32) -> (result: bool) while i < str.len() invariant forall|m: int| 0 <= m < i ==> (str[m] != key), + decreases + str.len() - i, + { if (str[i] == key) { return true; @@ -69,6 +72,8 @@ fn remove_elements(arr1: &Vec, arr2: &Vec) -> (result: Vec) 0 <= k < index ==> (arr2@.contains(#[trigger] arr1[k]) || output_str@.contains( #[trigger] arr1[k], )), + decreases + arr1.len() - index, { if (!contains(arr2, arr1[index])) { proof { diff --git a/benchmarks/MBPP/verified/task_id_170.rs b/benchmarks/MBPP/verified/task_id_170.rs index 63b78631..f4143f13 100644 --- a/benchmarks/MBPP/verified/task_id_170.rs +++ b/benchmarks/MBPP/verified/task_id_170.rs @@ -49,6 +49,8 @@ fn sum_range_list(arr: &Vec, start: usize, end: usize) -> (sum: i128) start <= j <= index ==> (i64::MIN * index <= (sum_to( #[trigger] arr@.subrange(start as int, j), )) <= i64::MAX * index), + decreases + _end - index, { assert(arr@.subrange(start as int, index as int) =~= arr@.subrange( start as int, diff --git a/benchmarks/MBPP/verified/task_id_18.rs b/benchmarks/MBPP/verified/task_id_18.rs index 61fb0c3d..bb32b378 100644 --- a/benchmarks/MBPP/verified/task_id_18.rs +++ b/benchmarks/MBPP/verified/task_id_18.rs @@ -51,6 +51,8 @@ fn contains(str: &Vec, key: char) -> (result: bool) while i < str.len() invariant forall|m: int| 0 <= m < i ==> (str[m] != key), + decreases + str.len() - i, { if (str[i] == key) { return true; @@ -84,6 +86,8 @@ fn remove_chars(str1: &Vec, str2: &Vec) -> (result: Vec) 0 <= k < index ==> (str2@.contains(#[trigger] str1[k]) || output_str@.contains( #[trigger] str1[k], )), + decreases + str1.len() - index, { if (!contains(str2, str1[index])) { proof { diff --git a/benchmarks/MBPP/verified/task_id_2.rs b/benchmarks/MBPP/verified/task_id_2.rs index 7e09ee8c..cece7ebc 100644 --- a/benchmarks/MBPP/verified/task_id_2.rs +++ b/benchmarks/MBPP/verified/task_id_2.rs @@ -27,6 +27,8 @@ fn contains(arr: &Vec, key: i32) -> (result: bool) while i < arr.len() invariant forall|m: int| 0 <= m < i ==> (arr[m] != key), + decreases + arr.len() - i, { if (arr[i] == key) { return true; @@ -55,6 +57,8 @@ fn shared_elements(list1: &Vec, list2: &Vec) -> (shared: Vec) #[trigger] shared[i], )), forall|m: int, n: int| 0 <= m < n < shared.len() ==> shared[m] != shared[n], + decreases + list1.len() - index, { if (contains(list2, list1[index]) && !contains(&shared, list1[index])) { shared.push(list1[index]); diff --git a/benchmarks/MBPP/verified/task_id_230.rs b/benchmarks/MBPP/verified/task_id_230.rs index 74432d0e..918ffe9b 100644 --- a/benchmarks/MBPP/verified/task_id_230.rs +++ b/benchmarks/MBPP/verified/task_id_230.rs @@ -47,6 +47,8 @@ fn replace_blanks_with_chars(str1: &Vec, ch: char) -> (result: Vec) } else { str1[k] }), + decreases + str1.len() - index, { if (str1[index] == ' ') { out_str.push(ch); diff --git a/benchmarks/MBPP/verified/task_id_240.rs b/benchmarks/MBPP/verified/task_id_240.rs index b6a826b6..7020c0c8 100644 --- a/benchmarks/MBPP/verified/task_id_240.rs +++ b/benchmarks/MBPP/verified/task_id_240.rs @@ -34,6 +34,8 @@ fn replace_last_element(first: &Vec, second: &Vec) -> (replaced_list: first_end == first.len() - 1, 0 <= index <= first_end, replaced_list@ =~= first@.subrange(0, index as int), + decreases + first_end - index, { replaced_list.push(first[index]); index += 1; @@ -45,6 +47,8 @@ fn replace_last_element(first: &Vec, second: &Vec) -> (replaced_list: replaced_list@ =~= first@.subrange(0, first.len() - 1).add( second@.subrange(0, index as int), ), + decreases + second.len() - index, { replaced_list.push(second[index]); index += 1; diff --git a/benchmarks/MBPP/verified/task_id_249.rs b/benchmarks/MBPP/verified/task_id_249.rs index aae85060..2ed45b52 100644 --- a/benchmarks/MBPP/verified/task_id_249.rs +++ b/benchmarks/MBPP/verified/task_id_249.rs @@ -27,6 +27,9 @@ fn contains(arr: &Vec, key: i32) -> (result: bool) while i < arr.len() invariant forall|m: int| 0 <= m < i ==> (arr[m] != key), + decreases + arr.len() - i, + { if (arr[i] == key) { return true; @@ -54,6 +57,8 @@ fn intersection(arr1: &Vec, arr2: &Vec) -> (result: Vec) 0 <= i < output_arr.len() ==> (arr1@.contains(#[trigger] output_arr[i]) && arr2@.contains(#[trigger] output_arr[i])), forall|m: int, n: int| 0 <= m < n < output_arr.len() ==> output_arr[m] != output_arr[n], + decreases + arr1.len() - index, { if (contains(arr2, arr1[index]) && !contains(&output_arr, arr1[index])) { output_arr.push(arr1[index]); diff --git a/benchmarks/MBPP/verified/task_id_251.rs b/benchmarks/MBPP/verified/task_id_251.rs index 4fefd53c..4f389940 100644 --- a/benchmarks/MBPP/verified/task_id_251.rs +++ b/benchmarks/MBPP/verified/task_id_251.rs @@ -35,6 +35,8 @@ fn insert_before_each(arr: &Vec, elem: i32) -> (result: Vec) result@.len() == index * 2, forall|k: int| 0 <= k < index ==> #[trigger] result[2 * k] == elem, forall|k: int| 0 <= k < index ==> #[trigger] result[2 * k + 1] == arr[k], + decreases + arr.len() - index, { result.push(elem); result.push(arr[index]); diff --git a/benchmarks/MBPP/verified/task_id_261.rs b/benchmarks/MBPP/verified/task_id_261.rs index d1a5764b..b2b6d6bb 100644 --- a/benchmarks/MBPP/verified/task_id_261.rs +++ b/benchmarks/MBPP/verified/task_id_261.rs @@ -46,6 +46,8 @@ fn element_wise_division(arr1: &Vec, arr2: &Vec) -> (result: Vec) <= u32::MAX), forall|k: int| 0 <= k < index ==> #[trigger] output_arr[k] == #[trigger] (arr1[k] / arr2[k]), + decreases + arr1.len() - index, { output_arr.push((arr1[index] / arr2[index])); index += 1; diff --git a/benchmarks/MBPP/verified/task_id_262.rs b/benchmarks/MBPP/verified/task_id_262.rs index 37bba493..4a780414 100644 --- a/benchmarks/MBPP/verified/task_id_262.rs +++ b/benchmarks/MBPP/verified/task_id_262.rs @@ -34,6 +34,8 @@ fn split_array(list: &Vec, l: usize) -> (new_list: (Vec, Vec)) 0 < l < list@.len(), 0 <= index <= l, part1@ =~= list@.subrange(0, index as int), + decreases + l - index, { part1.push(list[index]); index += 1; @@ -44,6 +46,8 @@ fn split_array(list: &Vec, l: usize) -> (new_list: (Vec, Vec)) invariant l <= index <= list.len(), part2@ =~= list@.subrange(l as int, index as int), + decreases + list.len() - index, { part2.push(list[index]); index += 1; diff --git a/benchmarks/MBPP/verified/task_id_273.rs b/benchmarks/MBPP/verified/task_id_273.rs index fb198e96..c959bb87 100644 --- a/benchmarks/MBPP/verified/task_id_273.rs +++ b/benchmarks/MBPP/verified/task_id_273.rs @@ -40,6 +40,8 @@ fn element_wise_subtract(arr1: &Vec, arr2: &Vec) -> (result: Vec) (0 <= i < arr1.len()) ==> (i32::MIN <= #[trigger] (arr1[i] - arr2[i]) <= i32::MAX), forall|k: int| 0 <= k < index ==> #[trigger] output_arr[k] == #[trigger] (arr1[k] - arr2[k]), + decreases + arr1.len() - index, { output_arr.push((arr1[index] - arr2[index])); index += 1; diff --git a/benchmarks/MBPP/verified/task_id_282.rs b/benchmarks/MBPP/verified/task_id_282.rs index edc7ca25..0c0835c2 100644 --- a/benchmarks/MBPP/verified/task_id_282.rs +++ b/benchmarks/MBPP/verified/task_id_282.rs @@ -38,6 +38,9 @@ fn element_wise_subtract(arr1: &Vec, arr2: &Vec) -> (result: Vec) (0 <= i < arr1.len()) ==> (i32::MIN <= #[trigger] (arr1[i] - arr2[i]) <= i32::MAX), forall|k: int| 0 <= k < index ==> #[trigger] output_arr[k] == #[trigger] (arr1[k] - arr2[k]), + decreases + arr1.len() - index, + { output_arr.push((arr1[index] - arr2[index])); index += 1; diff --git a/benchmarks/MBPP/verified/task_id_284.rs b/benchmarks/MBPP/verified/task_id_284.rs index e2f86cd3..1afd18ac 100644 --- a/benchmarks/MBPP/verified/task_id_284.rs +++ b/benchmarks/MBPP/verified/task_id_284.rs @@ -19,6 +19,8 @@ fn all_elements_equals(arr: &Vec, element: i32) -> (result: bool) invariant 0 <= index <= arr.len(), forall|k: int| 0 <= k < index ==> (arr[k] == element), + decreases + arr.len() - index, { if arr[index] != element { return false; diff --git a/benchmarks/MBPP/verified/task_id_290.rs b/benchmarks/MBPP/verified/task_id_290.rs index 5994d681..0bff0849 100644 --- a/benchmarks/MBPP/verified/task_id_290.rs +++ b/benchmarks/MBPP/verified/task_id_290.rs @@ -43,6 +43,8 @@ fn max_length_list(seq: &Vec>) -> (max_list: &Vec) 0 <= index <= seq.len(), forall|k: int| 0 <= k < index ==> max_list.len() >= #[trigger] (seq[k]).len(), exists|k: int| 0 <= k < index && max_list@ =~= #[trigger] (seq[k]@), + decreases + seq.len() - index, { if ((seq[index]).len() > max_list.len()) { max_list = &seq[index]; diff --git a/benchmarks/MBPP/verified/task_id_3.rs b/benchmarks/MBPP/verified/task_id_3.rs index 6b35d166..04f10f93 100644 --- a/benchmarks/MBPP/verified/task_id_3.rs +++ b/benchmarks/MBPP/verified/task_id_3.rs @@ -33,6 +33,8 @@ fn is_non_prime(n: u64) -> (result: bool) invariant 2 <= index, forall|k: int| 2 <= k < index ==> !is_divisible(n as int, k), + decreases + n - index, { if ((n % index) == 0) { assert(is_divisible(n as int, index as int)); diff --git a/benchmarks/MBPP/verified/task_id_307.rs b/benchmarks/MBPP/verified/task_id_307.rs index 245f9316..252d9438 100644 --- a/benchmarks/MBPP/verified/task_id_307.rs +++ b/benchmarks/MBPP/verified/task_id_307.rs @@ -25,6 +25,8 @@ fn list_deep_clone(arr: &Vec) -> (copied: Vec) 0 <= index <= arr.len(), copied_array.len() == index, forall|i: int| (0 <= i < index) ==> arr[i] == copied_array[i], + decreases + arr.len() - index, { copied_array.push(arr[index]); index += 1; diff --git a/benchmarks/MBPP/verified/task_id_399.rs b/benchmarks/MBPP/verified/task_id_399.rs index 905af7d1..25e84456 100644 --- a/benchmarks/MBPP/verified/task_id_399.rs +++ b/benchmarks/MBPP/verified/task_id_399.rs @@ -36,6 +36,8 @@ fn bit_wise_xor(arr1: &Vec, arr2: &Vec) -> (result: Vec) output_arr.len() == index, forall|k: int| 0 <= k < index ==> output_arr[k] == #[trigger] arr1[k] ^ #[trigger] arr2[k], + decreases + arr1.len() - index, { output_arr.push((arr1[index] ^ arr2[index])); index += 1; diff --git a/benchmarks/MBPP/verified/task_id_412.rs b/benchmarks/MBPP/verified/task_id_412.rs index 65d40c7e..8ec4a704 100644 --- a/benchmarks/MBPP/verified/task_id_412.rs +++ b/benchmarks/MBPP/verified/task_id_412.rs @@ -23,6 +23,8 @@ fn remove_odds(arr: &Vec) -> (even_list: Vec) invariant 0 <= index <= arr.len(), even_list@ == arr@.take(index as int).filter(|x: u32| x % 2 == 0), + decreases + arr.len() - index, { if (arr[index] % 2 == 0) { even_list.push(arr[index]); diff --git a/benchmarks/MBPP/verified/task_id_414.rs b/benchmarks/MBPP/verified/task_id_414.rs index 13378a74..a4dea1d4 100644 --- a/benchmarks/MBPP/verified/task_id_414.rs +++ b/benchmarks/MBPP/verified/task_id_414.rs @@ -19,6 +19,8 @@ fn contains(arr: &Vec, key: i32) -> (result: bool) invariant 0 <= i <= arr.len(), forall|m: int| 0 <= m < i ==> (arr[m] != key), + decreases + arr.len() - i, { if (arr[i] == key) { return true; @@ -37,6 +39,8 @@ fn any_value_exists(arr1: &Vec, arr2: &Vec) -> (result: bool) invariant 0 <= index <= arr1.len(), forall|k: int| 0 <= k < index ==> !arr2@.contains(#[trigger] arr1[k]), + decreases + arr1.len() - index, { if (contains(arr2, arr1[index])) { return true; diff --git a/benchmarks/MBPP/verified/task_id_424.rs b/benchmarks/MBPP/verified/task_id_424.rs index 24316a39..d0c827bd 100644 --- a/benchmarks/MBPP/verified/task_id_424.rs +++ b/benchmarks/MBPP/verified/task_id_424.rs @@ -52,6 +52,8 @@ fn extract_rear_chars(s: &Vec>) -> (result: Vec) rear_chars.len() == index, forall|i: int| 0 <= i < s.len() ==> #[trigger] s[i].len() > 0, forall|k: int| 0 <= k < index ==> rear_chars[k] == #[trigger] s[k][s[k].len() - 1], + decreases + s.len() - index, { let seq = &s[index]; rear_chars.push(seq[seq.len() - 1]); diff --git a/benchmarks/MBPP/verified/task_id_426.rs b/benchmarks/MBPP/verified/task_id_426.rs index bdef47cc..6b526cb0 100644 --- a/benchmarks/MBPP/verified/task_id_426.rs +++ b/benchmarks/MBPP/verified/task_id_426.rs @@ -29,6 +29,8 @@ fn filter_odd_numbers(arr: &Vec) -> (odd_list: Vec) invariant 0 <= index <= arr.len(), odd_list@ == arr@.take(index as int).filter(|x: u32| x % 2 != 0), + decreases + arr.len() - index, { if (arr[index] % 2 != 0) { odd_list.push(arr[index]); diff --git a/benchmarks/MBPP/verified/task_id_431.rs b/benchmarks/MBPP/verified/task_id_431.rs index 3b3d7835..58976f09 100644 --- a/benchmarks/MBPP/verified/task_id_431.rs +++ b/benchmarks/MBPP/verified/task_id_431.rs @@ -23,6 +23,8 @@ fn has_common_element(list1: &Vec, list2: &Vec) -> (result: bool) invariant 0 <= i <= list1.len(), forall|k: int, j: int| 0 <= k < i && 0 <= j < list2.len() ==> (list1[k] != list2[j]), + decreases + list1.len() - i, { let mut j = 0; while j < list2.len() @@ -30,6 +32,8 @@ fn has_common_element(list1: &Vec, list2: &Vec) -> (result: bool) 0 <= i < list1.len(), 0 <= j <= list2.len(), forall|k: int| 0 <= k < j ==> (list1[i as int] != list2[k]), + decreases + list2.len() - j, { if list1[i] == list2[j] { return true; diff --git a/benchmarks/MBPP/verified/task_id_433.rs b/benchmarks/MBPP/verified/task_id_433.rs index 606695a2..3c4256eb 100644 --- a/benchmarks/MBPP/verified/task_id_433.rs +++ b/benchmarks/MBPP/verified/task_id_433.rs @@ -19,6 +19,8 @@ fn is_greater(arr: &Vec, number: i32) -> (result: bool) invariant 0 <= i <= arr.len(), forall|k: int| 0 <= k < i ==> number > arr[k], + decreases + arr.len() - i, { if number <= arr[i] { return false; diff --git a/benchmarks/MBPP/verified/task_id_436.rs b/benchmarks/MBPP/verified/task_id_436.rs index 1f8d9b23..2e62c262 100644 --- a/benchmarks/MBPP/verified/task_id_436.rs +++ b/benchmarks/MBPP/verified/task_id_436.rs @@ -23,6 +23,8 @@ fn find_negative_numbers(arr: &Vec) -> (negative_list: Vec) invariant 0 <= index <= arr.len(), negative_list@ == arr@.take(index as int).filter(|x: i32| x < 0), + decreases + arr.len() - index, { if (arr[index] < 0) { negative_list.push(arr[index]); diff --git a/benchmarks/MBPP/verified/task_id_445.rs b/benchmarks/MBPP/verified/task_id_445.rs index 29f71d68..a4b38410 100644 --- a/benchmarks/MBPP/verified/task_id_445.rs +++ b/benchmarks/MBPP/verified/task_id_445.rs @@ -49,6 +49,8 @@ fn element_wise_multiplication(arr1: &Vec, arr2: &Vec) -> (result: Vec (0 <= i < arr1.len()) ==> (i32::MIN <= #[trigger] (arr1[i] * arr2[i]) <= i32::MAX), forall|k: int| 0 <= k < index ==> #[trigger] output_arr[k] == #[trigger] (arr1[k] * arr2[k]), + decreases + arr1.len() - index, { output_arr.push((arr1[index] * arr2[index])); index += 1; diff --git a/benchmarks/MBPP/verified/task_id_447.rs b/benchmarks/MBPP/verified/task_id_447.rs index aec652d3..4d644b18 100644 --- a/benchmarks/MBPP/verified/task_id_447.rs +++ b/benchmarks/MBPP/verified/task_id_447.rs @@ -39,6 +39,8 @@ fn cube_element(nums: &Vec) -> (cubed: Vec) * #[trigger] nums[k] <= i32::MAX), forall|k: int| 0 <= k < i ==> (#[trigger] cubed_array[k] == nums[k] * nums[k] * nums[k]), + decreases + nums.len() - i, { cubed_array.push(nums[i] * nums[i] * nums[i]); i += 1; diff --git a/benchmarks/MBPP/verified/task_id_454.rs b/benchmarks/MBPP/verified/task_id_454.rs index c6741191..d4d8b1de 100644 --- a/benchmarks/MBPP/verified/task_id_454.rs +++ b/benchmarks/MBPP/verified/task_id_454.rs @@ -19,6 +19,8 @@ fn contains_z(text: &Vec) -> (result: bool) invariant 0 <= index <= text.len(), forall|k: int| 0 <= k < index ==> (text[k] != 'Z' && text[k] != 'z'), + decreases + text.len() - index, { if text[index] == 'Z' || text[index] == 'z' { return true; diff --git a/benchmarks/MBPP/verified/task_id_457.rs b/benchmarks/MBPP/verified/task_id_457.rs index 1c24aa36..f08e4f49 100644 --- a/benchmarks/MBPP/verified/task_id_457.rs +++ b/benchmarks/MBPP/verified/task_id_457.rs @@ -35,6 +35,8 @@ fn min_sublist(seq: &Vec>) -> (min_list: &Vec) 0 <= index <= seq.len(), forall|k: int| 0 <= k < index ==> min_list.len() <= #[trigger] (seq[k]).len(), exists|k: int| 0 <= k < index && min_list@ =~= #[trigger] (seq[k]@), + decreases + seq.len() - index, { if ((seq[index]).len() < min_list.len()) { min_list = &seq[index]; diff --git a/benchmarks/MBPP/verified/task_id_460.rs b/benchmarks/MBPP/verified/task_id_460.rs index 90d16175..c0f21263 100644 --- a/benchmarks/MBPP/verified/task_id_460.rs +++ b/benchmarks/MBPP/verified/task_id_460.rs @@ -28,6 +28,8 @@ fn get_first_elements(arr: &Vec>) -> (result: Vec) first_elem_arr.len() == index, forall|i: int| 0 <= i < arr.len() ==> #[trigger] arr[i].len() > 0, forall|k: int| 0 <= k < index ==> #[trigger] first_elem_arr[k] == #[trigger] arr[k][0], + decreases + arr.len() - index, { let seq = &arr[index]; assert(seq.len() > 0); diff --git a/benchmarks/MBPP/verified/task_id_461.rs b/benchmarks/MBPP/verified/task_id_461.rs index 734d2b4d..daecd2d2 100644 --- a/benchmarks/MBPP/verified/task_id_461.rs +++ b/benchmarks/MBPP/verified/task_id_461.rs @@ -45,6 +45,8 @@ fn count_uppercase(text: &Vec) -> (count: u64) 0 <= index <= text.len(), 0 <= count <= index, count_uppercase_recursively(text@.subrange(0, index as int)) == count, + decreases + text.len() - index, { if ((text[index] as u32) >= 65 && (text[index] as u32) <= 90) { count += 1; diff --git a/benchmarks/MBPP/verified/task_id_472.rs b/benchmarks/MBPP/verified/task_id_472.rs index 58068d8d..59b8e9c0 100644 --- a/benchmarks/MBPP/verified/task_id_472.rs +++ b/benchmarks/MBPP/verified/task_id_472.rs @@ -24,6 +24,8 @@ fn contains_consecutive_numbers(arr: &Vec) -> (is_consecutive: bool) 0 <= index <= arr.len() - 1, forall|k: int| 0 <= k < arr.len() ==> (0 <= #[trigger] arr[k] + 1 < i32::MAX), forall|k: int, l: int| (0 <= k < l <= index && l == k + 1) ==> (arr[k] + 1 == arr[l]), + decreases + arr.len() - 1 - index, { if (arr[index] + 1 != arr[index + 1]) { return false; diff --git a/benchmarks/MBPP/verified/task_id_474.rs b/benchmarks/MBPP/verified/task_id_474.rs index 7e4ea5f9..383e63e2 100644 --- a/benchmarks/MBPP/verified/task_id_474.rs +++ b/benchmarks/MBPP/verified/task_id_474.rs @@ -47,6 +47,8 @@ fn replace_chars(str1: &Vec, old_char: char, new_char: char) -> (result: V } else { str1[k] }), + decreases + str1.len() - index, { if str1[index] == old_char { result_str.push(new_char); diff --git a/benchmarks/MBPP/verified/task_id_476.rs b/benchmarks/MBPP/verified/task_id_476.rs index a0fdbbc0..5daf9066 100644 --- a/benchmarks/MBPP/verified/task_id_476.rs +++ b/benchmarks/MBPP/verified/task_id_476.rs @@ -50,6 +50,8 @@ fn sum_min_max(arr: &Vec) -> (sum: i32) i32::MIN / 2 < max_val < i32::MAX / 2, max_val == max_rcur(arr@.subrange(0, index as int)), min_val == min_rcur(arr@.subrange(0, index as int)), + decreases + arr.len() - index, { if (arr[index] <= min_val) { min_val = arr[index]; diff --git a/benchmarks/MBPP/verified/task_id_477.rs b/benchmarks/MBPP/verified/task_id_477.rs index c5df4a4c..15c2012c 100644 --- a/benchmarks/MBPP/verified/task_id_477.rs +++ b/benchmarks/MBPP/verified/task_id_477.rs @@ -55,6 +55,8 @@ fn to_lowercase(str1: &Vec) -> (result: Vec) } else { str1[i] }), + decreases + str1.len() - index, { if (str1[index] >= 'A' && str1[index] <= 'Z') { lower_case.push(((str1[index] as u8) + 32) as char); diff --git a/benchmarks/MBPP/verified/task_id_554.rs b/benchmarks/MBPP/verified/task_id_554.rs index 457d4281..5f66dc5a 100644 --- a/benchmarks/MBPP/verified/task_id_554.rs +++ b/benchmarks/MBPP/verified/task_id_554.rs @@ -23,6 +23,8 @@ fn find_odd_numbers(arr: &Vec) -> (odd_numbers: Vec) invariant 0 <= index <= arr.len(), odd_numbers@ == arr@.take(index as int).filter(|x: u32| x % 2 != 0), + decreases + arr.len() - index, { if (arr[index] % 2 != 0) { odd_numbers.push(arr[index]); diff --git a/benchmarks/MBPP/verified/task_id_557.rs b/benchmarks/MBPP/verified/task_id_557.rs index ca93d935..7d3e3130 100644 --- a/benchmarks/MBPP/verified/task_id_557.rs +++ b/benchmarks/MBPP/verified/task_id_557.rs @@ -65,6 +65,8 @@ fn to_toggle_case(str1: &Vec) -> (toggle_case: Vec) toggle_case.len() == index, forall|i: int| 0 <= i < index ==> toggle_case[i] == to_toggle_case_spec(#[trigger] str1[i]), + decreases + str1.len() - index, { if (str1[index] >= 'a' && str1[index] <= 'z') { toggle_case.push(((str1[index] as u8) - 32) as char); diff --git a/benchmarks/MBPP/verified/task_id_567.rs b/benchmarks/MBPP/verified/task_id_567.rs index ede23807..27975d4a 100644 --- a/benchmarks/MBPP/verified/task_id_567.rs +++ b/benchmarks/MBPP/verified/task_id_567.rs @@ -21,6 +21,8 @@ fn is_sorted(arr: &Vec) -> (is_sorted: bool) invariant 0 <= index <= arr.len() - 1, forall|k: int, l: int| 0 <= k < l <= index ==> arr[k] <= arr[l], + decreases + arr.len() - 1 - index, { if arr[index] > arr[index + 1] { return false; diff --git a/benchmarks/MBPP/verified/task_id_572.rs b/benchmarks/MBPP/verified/task_id_572.rs index cb4060fc..20f9b916 100644 --- a/benchmarks/MBPP/verified/task_id_572.rs +++ b/benchmarks/MBPP/verified/task_id_572.rs @@ -35,6 +35,8 @@ fn count_frequency(arr: &Vec, key: i32) -> (frequency: usize) 0 <= index <= arr.len(), 0 <= counter <= index, count_frequency_rcr(arr@.subrange(0, index as int), key) == counter, + decreases + arr.len() - index, { if (arr[index] == key) { counter += 1; @@ -64,6 +66,8 @@ fn remove_duplicates(arr: &Vec) -> (unique_arr: Vec) unique_arr@ == arr@.take(index as int).filter( |x: i32| count_frequency_rcr(arr@, x) == 1, ), + decreases + arr.len() - index, { if count_frequency(&arr, arr[index]) == 1 { unique_arr.push(arr[index]); diff --git a/benchmarks/MBPP/verified/task_id_576.rs b/benchmarks/MBPP/verified/task_id_576.rs index 79390127..9547fd3e 100644 --- a/benchmarks/MBPP/verified/task_id_576.rs +++ b/benchmarks/MBPP/verified/task_id_576.rs @@ -37,6 +37,8 @@ fn sub_array_at_index(main: &Vec, sub: &Vec, idx: usize) -> (result: b forall|k: int| 0 <= k < i ==> main[idx + k] == sub[k], forall|k: int| 0 <= k < i ==> (main@.subrange(idx as int, (idx + k)) =~= sub@.subrange(0, k)), + decreases + sub.len() - i, { if (main[idx + i] != sub[i]) { assert(exists|k: int| 0 <= k < i ==> main[idx + k] != sub[k]); @@ -71,6 +73,8 @@ fn is_sub_array(main: &Vec, sub: &Vec) -> (result: bool) forall|k: int, l: int| (0 <= k < index) && l == k + sub.len() ==> (#[trigger] (main@.subrange(k, l)) != sub@), + decreases + (main.len() - sub.len()) + 1 - index, { if (sub_array_at_index(&main, &sub, index)) { return true; diff --git a/benchmarks/MBPP/verified/task_id_576_v2.rs b/benchmarks/MBPP/verified/task_id_576_v2.rs index c9154b03..6e6909a4 100644 --- a/benchmarks/MBPP/verified/task_id_576_v2.rs +++ b/benchmarks/MBPP/verified/task_id_576_v2.rs @@ -35,6 +35,8 @@ fn sub_array_at_index(main: &Vec, sub: &Vec, idx: usize) -> (result: b 0 <= idx <= (main.len() - sub.len()), 0 <= i <= sub.len(), forall|k: int| 0 <= k < i ==> main[idx + k] == sub[k], + decreases + sub.len() - i, { if (main[idx + i] != sub[i]) { return false; @@ -63,6 +65,8 @@ fn is_sub_array(main: &Vec, sub: &Vec) -> (result: bool) sub.len() <= main.len(), 0 <= index <= (main.len() - sub.len()) + 1, forall |k:int| 0<= k < index ==> !is_subrange_at(main@, sub@, k), + decreases + (main.len() - sub.len()) + 1 - index, { if (sub_array_at_index(&main, &sub, index)) { assert(is_subrange_at(main@, sub@, index as int)); diff --git a/benchmarks/MBPP/verified/task_id_578.rs b/benchmarks/MBPP/verified/task_id_578.rs index a650fb23..27285ed4 100644 --- a/benchmarks/MBPP/verified/task_id_578.rs +++ b/benchmarks/MBPP/verified/task_id_578.rs @@ -45,6 +45,8 @@ fn interleave(s1: &Vec, s2: &Vec, s3: &Vec) -> (res: Vec) forall|k: int| 0 <= k < index ==> (output_seq[3 * k] == s1[k] && output_seq[3 * k + 1] == s2[k] && output_seq[3 * k + 2] == s3[k]), + decreases + s1.len() - index, { output_seq.push(s1[index]); output_seq.push(s2[index]); diff --git a/benchmarks/MBPP/verified/task_id_579.rs b/benchmarks/MBPP/verified/task_id_579.rs index 6ca4d19b..453c15a1 100644 --- a/benchmarks/MBPP/verified/task_id_579.rs +++ b/benchmarks/MBPP/verified/task_id_579.rs @@ -36,6 +36,8 @@ fn contains(arr: &Vec, key: i32) -> (result: bool) while index < arr.len() invariant forall|m: int| 0 <= m < index ==> (arr[m] != key), + decreases + arr.len() - index, { if (arr[index] == key) { return true; @@ -70,6 +72,8 @@ fn find_dissimilar(arr1: &Vec, arr2: &Vec) -> (result: Vec) )), forall|m: int, n: int| 0 <= m < n < result.len() ==> #[trigger] result[m] != #[trigger] result[n], + decreases + arr1.len() - index, { if (!contains(arr2, arr1[index]) && !contains(&result, arr1[index])) { proof { @@ -94,6 +98,8 @@ fn find_dissimilar(arr1: &Vec, arr2: &Vec) -> (result: Vec) )), forall|m: int, n: int| 0 <= m < n < result.len() ==> #[trigger] result[m] != #[trigger] result[n], + decreases + arr2.len() - index, { if (!contains(arr1, arr2[index]) && !contains(&result, arr2[index])) { proof { diff --git a/benchmarks/MBPP/verified/task_id_586.rs b/benchmarks/MBPP/verified/task_id_586.rs index baf2b175..0f362f38 100644 --- a/benchmarks/MBPP/verified/task_id_586.rs +++ b/benchmarks/MBPP/verified/task_id_586.rs @@ -28,6 +28,8 @@ fn split_and_append(list: &Vec, n: usize) -> (new_list: Vec) invariant n <= index <= list.len(), list@.subrange(n as int, index as int) =~= new_list@, + decreases + list.len() - index, { new_list.push(list[index]); index += 1; @@ -40,6 +42,8 @@ fn split_and_append(list: &Vec, n: usize) -> (new_list: Vec) new_list@ =~= list@.subrange(n as int, list@.len() as int).add( list@.subrange(0, index as int), ), + decreases + n - index, { new_list.push(list[index]); index += 1; diff --git a/benchmarks/MBPP/verified/task_id_588.rs b/benchmarks/MBPP/verified/task_id_588.rs index 7e8ab05a..d00bf6e8 100644 --- a/benchmarks/MBPP/verified/task_id_588.rs +++ b/benchmarks/MBPP/verified/task_id_588.rs @@ -50,6 +50,8 @@ fn difference_max_min(arr: &Vec) -> (diff: i32) i32::MIN / 2 < max_val < i32::MAX / 2, max_val == max_rcur(arr@.subrange(0, index as int)), min_val == min_rcur(arr@.subrange(0, index as int)), + decreases + arr.len() - index, { if (arr[index] <= min_val) { min_val = arr[index]; diff --git a/benchmarks/MBPP/verified/task_id_602.rs b/benchmarks/MBPP/verified/task_id_602.rs index 49ed6460..0b0e4e70 100644 --- a/benchmarks/MBPP/verified/task_id_602.rs +++ b/benchmarks/MBPP/verified/task_id_602.rs @@ -41,6 +41,8 @@ fn count_frequency(arr: &Vec, key: char) -> (frequency: usize) 0 <= index <= arr.len(), 0 <= counter <= index, count_frequency_rcr(arr@.subrange(0, index as int), key) == counter, + decreases + arr.len() - index, { if (arr[index] == key) { counter += 1; @@ -75,6 +77,8 @@ fn first_repeated_char(str1: &Vec) -> (repeated_char: Option<(usize, char) str1@.take(index as int) =~= str1@.take(index as int).filter( |x: char| count_frequency_rcr(str1@, x) <= 1, ), + decreases + str1.len() - index, { if count_frequency(&str1, str1[index]) > 1 { return Some((index, str1[index])); diff --git a/benchmarks/MBPP/verified/task_id_605.rs b/benchmarks/MBPP/verified/task_id_605.rs index 6397913d..a36e8c04 100644 --- a/benchmarks/MBPP/verified/task_id_605.rs +++ b/benchmarks/MBPP/verified/task_id_605.rs @@ -33,6 +33,8 @@ fn prime_num(n: u64) -> (result: bool) invariant 2 <= index <= n, forall|k: int| 2 <= k < index ==> !is_divisible(n as int, k), + decreases + n - index, { if ((n % index) == 0) { assert(is_divisible(n as int, index as int)); diff --git a/benchmarks/MBPP/verified/task_id_610.rs b/benchmarks/MBPP/verified/task_id_610.rs index 2b58df3c..dd3f2384 100644 --- a/benchmarks/MBPP/verified/task_id_610.rs +++ b/benchmarks/MBPP/verified/task_id_610.rs @@ -34,6 +34,8 @@ fn remove_kth_element(list: &Vec, k: usize) -> (new_list: Vec) 0 <= index <= k - 1, 0 < k < list@.len(), new_list@ =~= list@.subrange(0, index as int), + decreases + k - 1 - index, { new_list.push(list[index]); index += 1; @@ -45,6 +47,8 @@ fn remove_kth_element(list: &Vec, k: usize) -> (new_list: Vec) new_list@ =~= list@.subrange(0 as int, k - 1 as int).add( list@.subrange(k as int, index as int), ), + decreases + list.len() - index, { new_list.push(list[index]); index += 1; diff --git a/benchmarks/MBPP/verified/task_id_616.rs b/benchmarks/MBPP/verified/task_id_616.rs index 79ec8e2c..1bc4dfed 100644 --- a/benchmarks/MBPP/verified/task_id_616.rs +++ b/benchmarks/MBPP/verified/task_id_616.rs @@ -42,6 +42,8 @@ fn element_wise_module(arr1: &Vec, arr2: &Vec) -> (result: Vec) (0 <= i < arr1.len()) ==> (i32::MIN <= #[trigger] (arr1[i] % arr2[i]) <= i32::MAX), forall|k: int| 0 <= k < index ==> #[trigger] output_arr[k] == #[trigger] (arr1[k] % arr2[k]), + decreases + arr1.len() - index, { output_arr.push((arr1[index] % arr2[index])); index += 1; diff --git a/benchmarks/MBPP/verified/task_id_618.rs b/benchmarks/MBPP/verified/task_id_618.rs index 3780d967..ecb243cf 100644 --- a/benchmarks/MBPP/verified/task_id_618.rs +++ b/benchmarks/MBPP/verified/task_id_618.rs @@ -37,6 +37,8 @@ fn element_wise_divide(arr1: &Vec, arr2: &Vec) -> (result: Vec) (0 <= i < arr1.len()) ==> (i32::MIN <= #[trigger] (arr1[i] / arr2[i]) <= i32::MAX), forall|k: int| 0 <= k < index ==> #[trigger] output_arr[k] == #[trigger] (arr1[k] / arr2[k]), + decreases + arr1.len() - index, { output_arr.push((arr1[index] / arr2[index])); index += 1; diff --git a/benchmarks/MBPP/verified/task_id_62.rs b/benchmarks/MBPP/verified/task_id_62.rs index 8902c635..a68b61ff 100644 --- a/benchmarks/MBPP/verified/task_id_62.rs +++ b/benchmarks/MBPP/verified/task_id_62.rs @@ -25,6 +25,8 @@ fn smallest_num(nums: &Vec) -> (min: i32) 0 <= index <= nums.len(), forall|k: int| 0 <= k < index ==> min <= nums[k], exists|k: int| 0 <= k < index && min == nums[k], + decreases + nums.len() - index, { if nums[index] < min { min = nums[index]; diff --git a/benchmarks/MBPP/verified/task_id_624.rs b/benchmarks/MBPP/verified/task_id_624.rs index dd67cd57..b25472e7 100644 --- a/benchmarks/MBPP/verified/task_id_624.rs +++ b/benchmarks/MBPP/verified/task_id_624.rs @@ -55,6 +55,8 @@ fn to_uppercase(str1: &Vec) -> (result: Vec) } else { str1[i] })), + decreases + str1.len() - index, { if (str1[index] >= 'a' && str1[index] <= 'z') { upper_case.push(((str1[index] as u8) - 32) as char); diff --git a/benchmarks/MBPP/verified/task_id_629.rs b/benchmarks/MBPP/verified/task_id_629.rs index 1fa1a4c3..5763bb45 100644 --- a/benchmarks/MBPP/verified/task_id_629.rs +++ b/benchmarks/MBPP/verified/task_id_629.rs @@ -23,6 +23,8 @@ fn find_even_numbers(arr: &Vec) -> (even_numbers: Vec) invariant 0 <= index <= arr.len(), even_numbers@ == arr@.take(index as int).filter(|x: u32| x % 2 == 0), + decreases + arr.len() - index, { if (arr[index] % 2 == 0) { even_numbers.push(arr[index]); diff --git a/benchmarks/MBPP/verified/task_id_644.rs b/benchmarks/MBPP/verified/task_id_644.rs index 2dfef1e3..53e94a65 100644 --- a/benchmarks/MBPP/verified/task_id_644.rs +++ b/benchmarks/MBPP/verified/task_id_644.rs @@ -26,6 +26,8 @@ fn reverse_to_k(list: &Vec, n: usize) -> (reversed_list: Vec) 0 <= index <= n, reversed_list.len() == index, forall|k: int| 0 <= k < index ==> reversed_list[k] == list[n - 1 - k], + decreases + n - index, { reversed_list.push(list[n - 1 - index]); index += 1; @@ -37,6 +39,8 @@ fn reverse_to_k(list: &Vec, n: usize) -> (reversed_list: Vec) reversed_list@ =~= list@.subrange(0, n as int).reverse().add( list@.subrange(n as int, index as int), ), + decreases + list.len() - index, { reversed_list.push(list[index]); index += 1; diff --git a/benchmarks/MBPP/verified/task_id_69.rs b/benchmarks/MBPP/verified/task_id_69.rs index 902b9136..8c78fd37 100644 --- a/benchmarks/MBPP/verified/task_id_69.rs +++ b/benchmarks/MBPP/verified/task_id_69.rs @@ -26,6 +26,8 @@ fn is_sub_list_at_index(main: &Vec, sub: &Vec, idx: usize) -> (result: forall|k: int| 0 <= k < i ==> main[idx + k] == sub[k], forall|k: int| 0 <= k < i ==> (main@.subrange(idx as int, (idx + k)) =~= sub@.subrange(0, k)), + decreases + sub.len() - i, { if (main[idx + i] != sub[i]) { assert(exists|k: int| 0 <= k < i ==> main[idx + k] != sub[k]); @@ -59,6 +61,8 @@ fn is_sub_list(main: &Vec, sub: &Vec) -> (result: bool) forall|k: int, l: int| (0 <= k < index) && l == k + sub.len() ==> (#[trigger] (main@.subrange(k, l)) != sub@), + decreases + (main.len() - sub.len()) + 1 - index, { if (is_sub_list_at_index(&main, &sub, index)) { return true; diff --git a/benchmarks/MBPP/verified/task_id_70.rs b/benchmarks/MBPP/verified/task_id_70.rs index eeb875dd..18604bbe 100644 --- a/benchmarks/MBPP/verified/task_id_70.rs +++ b/benchmarks/MBPP/verified/task_id_70.rs @@ -27,6 +27,8 @@ fn all_sequence_equal_length(seq: &Vec>) -> (result: bool) invariant 1 <= index <= seq.len(), forall|k: int| 0 <= k < index ==> (#[trigger] seq[k].len() == (&seq[0]).len()), + decreases + seq.len() - index, { if ((&seq[index]).len() != (&seq[0]).len()) { return false; diff --git a/benchmarks/MBPP/verified/task_id_728.rs b/benchmarks/MBPP/verified/task_id_728.rs index fd744619..57e3f966 100644 --- a/benchmarks/MBPP/verified/task_id_728.rs +++ b/benchmarks/MBPP/verified/task_id_728.rs @@ -34,6 +34,8 @@ fn add_list(arr1: &Vec, arr2: &Vec) -> (result: Vec) (0 <= i < arr1.len()) ==> (i32::MIN <= #[trigger] (arr1[i] + arr2[i]) <= i32::MAX), forall|k: int| 0 <= k < index ==> #[trigger] output_arr[k] == #[trigger] (arr1[k] + arr2[k]), + decreases + arr1.len() - index, { output_arr.push((arr1[index] + arr2[index])); index += 1; diff --git a/benchmarks/MBPP/verified/task_id_732.rs b/benchmarks/MBPP/verified/task_id_732.rs index bee58004..276ceec8 100644 --- a/benchmarks/MBPP/verified/task_id_732.rs +++ b/benchmarks/MBPP/verified/task_id_732.rs @@ -51,6 +51,8 @@ fn replace_with_colon(str1: &Vec) -> (result: Vec) } else { str1[k] }), + decreases + str1.len() - index, { if ((str1[index] == ' ') || (str1[index] == ',') || (str1[index] == '.')) { result.push(':'); diff --git a/benchmarks/MBPP/verified/task_id_733.rs b/benchmarks/MBPP/verified/task_id_733.rs index a83c2723..57407cfc 100644 --- a/benchmarks/MBPP/verified/task_id_733.rs +++ b/benchmarks/MBPP/verified/task_id_733.rs @@ -39,6 +39,8 @@ fn find_first_occurrence(arr: &Vec, target: i32) -> (index: Option) while index < arr.len() invariant forall|k: int| 0 <= k < index ==> arr[k] != target, + decreases + arr.len() - index, { if arr[index] == target { return Some(index); diff --git a/benchmarks/MBPP/verified/task_id_741.rs b/benchmarks/MBPP/verified/task_id_741.rs index a1310966..25e4c001 100644 --- a/benchmarks/MBPP/verified/task_id_741.rs +++ b/benchmarks/MBPP/verified/task_id_741.rs @@ -23,6 +23,8 @@ fn all_characters_same(char_arr: &Vec) -> (result: bool) invariant 1 <= index <= char_arr.len(), forall|k: int| 0 <= k < index ==> char_arr[0] == #[trigger] char_arr[k], + decreases + char_arr.len() - index, { if char_arr[0] != char_arr[index] { assert(exists|i: int| diff --git a/benchmarks/MBPP/verified/task_id_743.rs b/benchmarks/MBPP/verified/task_id_743.rs index 8b2c17a2..d4ffb5a2 100644 --- a/benchmarks/MBPP/verified/task_id_743.rs +++ b/benchmarks/MBPP/verified/task_id_743.rs @@ -42,6 +42,8 @@ fn rotate_right(list: &Vec, n: usize) -> (new_list: Vec) invariant split_index <= index <= list.len(), list@.subrange(split_index as int, index as int) =~= new_list@, + decreases + list.len() - index, { new_list.push(list[index]); index += 1; @@ -54,6 +56,8 @@ fn rotate_right(list: &Vec, n: usize) -> (new_list: Vec) new_list@ =~= list@.subrange(split_index as int, list@.len() as int).add( list@.subrange(0, index as int), ), + decreases + split_index - index, { new_list.push(list[index]); index += 1; diff --git a/benchmarks/MBPP/verified/task_id_755.rs b/benchmarks/MBPP/verified/task_id_755.rs index 8d9ff93b..7060ad09 100644 --- a/benchmarks/MBPP/verified/task_id_755.rs +++ b/benchmarks/MBPP/verified/task_id_755.rs @@ -64,6 +64,8 @@ fn second_smallest(numbers: &Vec) -> (indices: ( forall|k: int| 0 <= k < index ==> numbers[k] >= numbers[min_index as int], forall|k: int| 0 <= k < index && k != min_index ==> numbers[k] >= numbers[second_min_index as int], + decreases + numbers.len() - index, { if numbers[index] < numbers[min_index] { second_min_index = min_index; diff --git a/benchmarks/MBPP/verified/task_id_760.rs b/benchmarks/MBPP/verified/task_id_760.rs index c6bf472e..fe70dc60 100644 --- a/benchmarks/MBPP/verified/task_id_760.rs +++ b/benchmarks/MBPP/verified/task_id_760.rs @@ -22,6 +22,8 @@ fn has_only_one_distinct_element(arr: &Vec) -> (result: bool) invariant 1 <= index <= arr.len(), forall|k: int| 0 <= k < index ==> arr[0] == #[trigger] arr[k], + decreases + arr.len() - index, { if arr[0] != arr[index] { assert(exists|i: int| 1 <= i < arr@.len() && arr[0] != #[trigger] arr[i]); diff --git a/benchmarks/MBPP/verified/task_id_764.rs b/benchmarks/MBPP/verified/task_id_764.rs index 1c803a92..ca521a10 100644 --- a/benchmarks/MBPP/verified/task_id_764.rs +++ b/benchmarks/MBPP/verified/task_id_764.rs @@ -42,6 +42,8 @@ fn count_digits(text: &Vec) -> (count: usize) 0 <= index <= text.len(), 0 <= count <= index, count == count_digits_recursively(text@.subrange(0, index as int)), + decreases + text.len() - index, { if ((text[index] as u8) >= 48 && (text[index] as u8) <= 57) { count += 1; diff --git a/benchmarks/MBPP/verified/task_id_769.rs b/benchmarks/MBPP/verified/task_id_769.rs index 60249414..6e8813f6 100644 --- a/benchmarks/MBPP/verified/task_id_769.rs +++ b/benchmarks/MBPP/verified/task_id_769.rs @@ -33,6 +33,8 @@ fn contains(arr: &Vec, key: i32) -> (result: bool) while index < arr.len() invariant forall|m: int| 0 <= m < index ==> (arr[m] != key), + decreases + arr.len() - index, { if (arr[index] == key) { return true; @@ -67,6 +69,8 @@ fn difference(arr1: &Vec, arr2: &Vec) -> (result: Vec) )), forall|m: int, n: int| 0 <= m < n < result.len() ==> #[trigger] result[m] != #[trigger] result[n], + decreases + arr1.len() - index, { if (!contains(arr2, arr1[index]) && !contains(&result, arr1[index])) { proof { @@ -90,6 +94,8 @@ fn difference(arr1: &Vec, arr2: &Vec) -> (result: Vec) )), forall|m: int, n: int| 0 <= m < n < result.len() ==> #[trigger] result[m] != #[trigger] result[n], + decreases + arr2.len() - index, { if (!contains(arr1, arr2[index]) && !contains(&result, arr2[index])) { proof { diff --git a/benchmarks/MBPP/verified/task_id_775.rs b/benchmarks/MBPP/verified/task_id_775.rs index 6031b3fc..8be18546 100644 --- a/benchmarks/MBPP/verified/task_id_775.rs +++ b/benchmarks/MBPP/verified/task_id_775.rs @@ -19,6 +19,8 @@ fn is_odd_at_odd_index(arr: &Vec) -> (result: bool) invariant 0 <= index <= arr.len(), forall|i: int| 0 <= i < index ==> ((i % 2) == (arr[i] % 2)), + decreases + arr.len() - index, { if ((index % 2) != (arr[index] % 2)) { assert(((index as int) % 2) != (arr[index as int] % 2)); diff --git a/benchmarks/MBPP/verified/task_id_790.rs b/benchmarks/MBPP/verified/task_id_790.rs index 028d3e91..711ae99a 100644 --- a/benchmarks/MBPP/verified/task_id_790.rs +++ b/benchmarks/MBPP/verified/task_id_790.rs @@ -19,6 +19,8 @@ fn is_even_at_even_index(arr: &Vec) -> (result: bool) invariant 0 <= index <= arr.len(), forall|i: int| 0 <= i < index ==> ((i % 2) == (arr[i] % 2)), + decreases + arr.len() - index, { if ((index % 2) != (arr[index] % 2)) { assert(((index as int) % 2) != (arr[index as int] % 2)); diff --git a/benchmarks/MBPP/verified/task_id_798.rs b/benchmarks/MBPP/verified/task_id_798.rs index 62ea7a59..b1bddadc 100644 --- a/benchmarks/MBPP/verified/task_id_798.rs +++ b/benchmarks/MBPP/verified/task_id_798.rs @@ -34,6 +34,8 @@ fn sum(arr: &Vec) -> (sum: i128) forall|j: int| 0 <= j <= index ==> (i64::MIN * index <= (sum_to(#[trigger] arr@.subrange(0, j))) <= i64::MAX * index), + decreases + arr.len() - index, { assert(arr@.subrange(0, index as int) =~= arr@.subrange(0, (index + 1) as int).drop_last()); sum = sum + arr[index] as i128; diff --git a/benchmarks/MBPP/verified/task_id_8.rs b/benchmarks/MBPP/verified/task_id_8.rs index 26654bc3..ff55a12a 100644 --- a/benchmarks/MBPP/verified/task_id_8.rs +++ b/benchmarks/MBPP/verified/task_id_8.rs @@ -31,6 +31,8 @@ fn square_nums(nums: &Vec) -> (squared: Vec) forall|k: int| 0 <= k < nums.len() ==> (0 <= #[trigger] nums[k] * #[trigger] nums[k] < i32::MAX), forall|k: int| 0 <= k < index ==> (#[trigger] result[k] == nums[k] * nums[k]), + decreases + nums.len() - index, { result.push(nums[index] * nums[index]); index += 1 diff --git a/benchmarks/MBPP/verified/task_id_804.rs b/benchmarks/MBPP/verified/task_id_804.rs index d0e4ca87..bac137e7 100644 --- a/benchmarks/MBPP/verified/task_id_804.rs +++ b/benchmarks/MBPP/verified/task_id_804.rs @@ -21,6 +21,8 @@ fn is_product_even(arr: &Vec) -> (result: bool) invariant 0 <= index <= arr.len(), forall|k: int| 0 <= k < index ==> !(is_even(#[trigger] arr[k])), + decreases + arr.len() - index, { if (arr[index] % 2 == 0) { return true; diff --git a/benchmarks/MBPP/verified/task_id_807.rs b/benchmarks/MBPP/verified/task_id_807.rs index 75b907ef..a38f3197 100644 --- a/benchmarks/MBPP/verified/task_id_807.rs +++ b/benchmarks/MBPP/verified/task_id_807.rs @@ -27,6 +27,8 @@ fn find_first_odd(arr: &Vec) -> (index: Option) invariant 0 <= index <= arr.len(), arr@.take(index as int) =~= arr@.take(index as int).filter(|x: u32| x % 2 == 0), + decreases + arr.len() - index, { if (arr[index] % 2 != 0) { return Some(index); diff --git a/benchmarks/MBPP/verified/task_id_808.rs b/benchmarks/MBPP/verified/task_id_808.rs index dce08ddf..2ec0678b 100644 --- a/benchmarks/MBPP/verified/task_id_808.rs +++ b/benchmarks/MBPP/verified/task_id_808.rs @@ -19,6 +19,8 @@ fn contains_k(arr: &Vec, k: i32) -> (result: bool) invariant 0 <= index <= arr.len(), forall|m: int| 0 <= m < index ==> (arr[m] != k), + decreases + arr.len() - index, { if (arr[index] == k) { return true; diff --git a/benchmarks/MBPP/verified/task_id_809.rs b/benchmarks/MBPP/verified/task_id_809.rs index 5954d6f4..e8559600 100644 --- a/benchmarks/MBPP/verified/task_id_809.rs +++ b/benchmarks/MBPP/verified/task_id_809.rs @@ -23,6 +23,8 @@ fn is_smaller(arr1: &Vec, arr2: &Vec) -> (result: bool) arr1.len() == arr2.len(), 0 <= index <= arr2.len(), forall|k: int| 0 <= k < index ==> arr1[k] > arr2[k], + decreases + arr1.len() - index, { if arr1[index] <= arr2[index] { return false; diff --git a/benchmarks/MBPP/verified/task_id_94.rs b/benchmarks/MBPP/verified/task_id_94.rs index 3bb11230..6b5710b9 100644 --- a/benchmarks/MBPP/verified/task_id_94.rs +++ b/benchmarks/MBPP/verified/task_id_94.rs @@ -37,6 +37,8 @@ fn min_second_value_first(arr: &Vec>) -> (first_of_min_second: i32) forall|i: int| 0 <= i < arr.len() ==> #[trigger] arr[i].len() >= 2, forall|k: int| 0 <= k < index ==> (arr[min_second_index as int][1] <= #[trigger] arr[k][1]), + decreases + arr.len() - index, { assert(arr[index as int].len() > 0); assert(arr[min_second_index as int].len() > 0); diff --git a/benchmarks/MBPP/verified/task_id_95.rs b/benchmarks/MBPP/verified/task_id_95.rs index d782c0d6..d08e9117 100644 --- a/benchmarks/MBPP/verified/task_id_95.rs +++ b/benchmarks/MBPP/verified/task_id_95.rs @@ -32,6 +32,8 @@ fn smallest_list_length(list: &Vec>) -> (min: usize) 0 <= index <= list.len(), forall|k: int| 0 <= k < index ==> min <= #[trigger] list[k].len(), exists|k: int| 0 <= k < index && min == #[trigger] list[k].len(), + decreases + list.len() - index, { if (&list[index]).len() < min { min = (&list[index]).len(); diff --git a/benchmarks/Misc/verified/arg_free.rs b/benchmarks/Misc/verified/arg_free.rs index 32170da8..2eacbc68 100644 --- a/benchmarks/Misc/verified/arg_free.rs +++ b/benchmarks/Misc/verified/arg_free.rs @@ -14,6 +14,8 @@ fn choose_odd() idx<=10, gap<100, gap==res-idx, + decreases + 10-idx, { res = res + 1; idx = idx + 1; @@ -27,6 +29,9 @@ fn choose_odd() idx<=10, gap<100, gap==res-idx, + decreases + 10-idx, + { res = res + 1; diff --git a/benchmarks/Misc/verified/binary_search.rs b/benchmarks/Misc/verified/binary_search.rs index 00d29fe1..852fb703 100644 --- a/benchmarks/Misc/verified/binary_search.rs +++ b/benchmarks/Misc/verified/binary_search.rs @@ -18,6 +18,8 @@ fn binary_search(v: &Vec, k: u64) -> (r: usize) i2 < v.len(), exists|i: int| i1 <= i <= i2 && k == v[i], forall|i: int, j: int| 0 <= i <= j < v.len() ==> v[i] <= v[j], + decreases + i2 - i1, { let ix = i1 + (i2 - i1) / 2; if v[ix] < k { diff --git a/benchmarks/Misc/verified/bubble_v1.rs b/benchmarks/Misc/verified/bubble_v1.rs index 3c34d8c6..1f74b823 100644 --- a/benchmarks/Misc/verified/bubble_v1.rs +++ b/benchmarks/Misc/verified/bubble_v1.rs @@ -38,6 +38,8 @@ verus! { forall|x: int, y: int| 0 <= x <= y <= i ==> x != j && y != j ==> nums[x] <= nums[y], sorted_between(nums@, j as int, i + 1), is_reorder_of(r, nums@, old(nums)@), + decreases + j, { if nums[j - 1] > nums[j] { let temp = nums[j - 1]; diff --git a/benchmarks/Misc/verified/bubble_v2.rs b/benchmarks/Misc/verified/bubble_v2.rs index ec9ec725..a50b5f88 100644 --- a/benchmarks/Misc/verified/bubble_v2.rs +++ b/benchmarks/Misc/verified/bubble_v2.rs @@ -41,6 +41,8 @@ verus! { forall|x: int, y: int| 0 <= x <= y <= i ==> x != j && y != j ==> nums[x] <= nums[y], sorted_between(nums@, j as int, i + 1), exists|r: Seq| is_reorder_of(r, nums@, old(nums)@), + decreases + j, { if nums[j - 1] > nums[j] { proof { diff --git a/benchmarks/Misc/verified/cell_2_sum.rs b/benchmarks/Misc/verified/cell_2_sum.rs index d2ca2352..41cedb28 100644 --- a/benchmarks/Misc/verified/cell_2_sum.rs +++ b/benchmarks/Misc/verified/cell_2_sum.rs @@ -14,6 +14,8 @@ pub fn myfun(a: &mut Vec, N: u32) -> (sum: u32) invariant a.len()==N, forall|j:int| 0<=j a[j]<=2, + decreases + N - i, { if (a[i] > 2) { a.set(i, 2); @@ -32,6 +34,9 @@ pub fn myfun(a: &mut Vec, N: u32) -> (sum: u32) a.len()==N, forall|j:int| 0<=j a[j]<=2, sum<=2 * i, + decreases + N - i, + { sum = sum + a[i]; i = i + 1; diff --git a/benchmarks/Misc/verified/choose_odd.rs b/benchmarks/Misc/verified/choose_odd.rs index 4bc7f2bf..e964c0ed 100644 --- a/benchmarks/Misc/verified/choose_odd.rs +++ b/benchmarks/Misc/verified/choose_odd.rs @@ -13,6 +13,8 @@ fn choose_odd(v: &Vec) -> (odd_index: usize) while (j < v.len()) invariant forall |q:int| 0<=q #[trigger] v[q]%2!=1, + decreases + v.len() - j, { if (v[j] % 2 == 1) { return j; diff --git a/benchmarks/Misc/verified/conditional_average.rs b/benchmarks/Misc/verified/conditional_average.rs index c539ffb9..27bcdc8c 100644 --- a/benchmarks/Misc/verified/conditional_average.rs +++ b/benchmarks/Misc/verified/conditional_average.rs @@ -36,6 +36,8 @@ fn conditional_average(vals_1: &Vec, vals_2: &Vec, conds_1: &Vec (conds_1[i] && !conds_2[i] ==> avgs[i] == vals_1[i]) && (!conds_1[i] && conds_2[i] ==> avgs[i] == vals_2[i]) ), + decreases + common_len - k, { let mut new_avg: u64 = 0; if (conds_1[k]) { diff --git a/benchmarks/Misc/verified/deduplicate.rs b/benchmarks/Misc/verified/deduplicate.rs index 540937ee..88cf06c0 100644 --- a/benchmarks/Misc/verified/deduplicate.rs +++ b/benchmarks/Misc/verified/deduplicate.rs @@ -71,6 +71,8 @@ ensures 0 <= i <= nums@.len(), nums@.subrange(0, i as int).to_set().ext_equal(res@.to_set()), res@.no_duplicates(), + decreases + nums.len() - i, { let mut found = false; let mut j = 0; diff --git a/benchmarks/Misc/verified/fib.rs b/benchmarks/Misc/verified/fib.rs index ed9eb74e..57540e34 100644 --- a/benchmarks/Misc/verified/fib.rs +++ b/benchmarks/Misc/verified/fib.rs @@ -50,6 +50,8 @@ ensures 2 <= i, fib@.len() == i, i <= n, + decreases + n - i, { proof{ fibo_is_monotonic(i as int, n as int); diff --git a/benchmarks/Misc/verified/filter.rs b/benchmarks/Misc/verified/filter.rs index dfe04bbf..13fd1d57 100644 --- a/benchmarks/Misc/verified/filter.rs +++ b/benchmarks/Misc/verified/filter.rs @@ -17,6 +17,8 @@ ensures 0 <= i <= xlen, x@.len() == xlen, // always specify the length of vectors used in the loop y@ == x@.take(i as int).filter(|k:u64| k%3 == 0),//routine for filter + decreases + xlen - i, { if (x[i] % 3 == 0) { y.push(x[i]); diff --git a/benchmarks/Misc/verified/filter_v2.rs b/benchmarks/Misc/verified/filter_v2.rs index 22ba4963..63871e59 100644 --- a/benchmarks/Misc/verified/filter_v2.rs +++ b/benchmarks/Misc/verified/filter_v2.rs @@ -34,6 +34,8 @@ ensures 0 <= i <= xlen, x@.len() == xlen, y@ == x@.take(i as int).filter(|k:u64| k%3 == 0), + decreases + xlen - i, { if (x[i] % 3 == 0) { y.push(x[i]); diff --git a/benchmarks/Misc/verified/filter_weak.rs b/benchmarks/Misc/verified/filter_weak.rs index bd0735ee..136d5867 100644 --- a/benchmarks/Misc/verified/filter_weak.rs +++ b/benchmarks/Misc/verified/filter_weak.rs @@ -17,6 +17,8 @@ ensures invariant x@.len() == xlen, // always specify the length of vectors used in the loop forall |k:int| 0 <= k < y.len() ==> y[k] % 3 == 0 && x@.contains(y@[k]), + decreases + xlen - i, { if (x[i] % 3 == 0) { y.push(x[i]); diff --git a/benchmarks/Misc/verified/findmax.rs b/benchmarks/Misc/verified/findmax.rs index 8e9afd18..8ec10673 100644 --- a/benchmarks/Misc/verified/findmax.rs +++ b/benchmarks/Misc/verified/findmax.rs @@ -16,6 +16,8 @@ ensures invariant forall |k: int| 0 <= k < i ==> nums@[k] <= max, exists |k: int| 0 <= k < i && nums@[k] == max, + decreases + nums.len() - i, { if nums[i] > max { max = nums[i]; diff --git a/benchmarks/Misc/verified/havoc_inline_post.rs b/benchmarks/Misc/verified/havoc_inline_post.rs index 7cff0f64..8569eaf9 100644 --- a/benchmarks/Misc/verified/havoc_inline_post.rs +++ b/benchmarks/Misc/verified/havoc_inline_post.rs @@ -19,6 +19,8 @@ pub fn havoc_inline_post(v: &mut Vec, a: u32, b: bool) forall |k:int| idx <= k < v.len() ==> v[k] == 1 + a, forall |k:int| 0 <= k < idx ==> v[k] == 1, 10 < a < 20, + decreases + idx, { idx = idx - 1; v.set(idx, v[idx] + a); diff --git a/benchmarks/Misc/verified/linearsearch.rs b/benchmarks/Misc/verified/linearsearch.rs index 252b36e5..c3dd9f88 100644 --- a/benchmarks/Misc/verified/linearsearch.rs +++ b/benchmarks/Misc/verified/linearsearch.rs @@ -20,6 +20,8 @@ ensures 0 <= i <= nums@.len(), ensures 0 <= i < nums@.len() ==> (#[trigger]nums@[i as int]) == target, + decreases + nums.len() - i, { if nums[i] == target { break; diff --git a/benchmarks/Misc/verified/map.rs b/benchmarks/Misc/verified/map.rs index 68f899e1..665a466a 100644 --- a/benchmarks/Misc/verified/map.rs +++ b/benchmarks/Misc/verified/map.rs @@ -16,6 +16,8 @@ ensures forall |k:int| 0 <= k < i ==> #[trigger] x[k] == old(x)[k] + 4, forall |k:int| i <= k < xlen ==> x[k] == old(x)[k], forall |k:int| 0 <= k < xlen ==> old(x)[k] <= 0x7FFF_FFFB, + decreases + xlen - i, { x.set(i, x[i] + 4); i = i + 1; diff --git a/benchmarks/Misc/verified/max_index.rs b/benchmarks/Misc/verified/max_index.rs index bc6a78d3..00edbb51 100644 --- a/benchmarks/Misc/verified/max_index.rs +++ b/benchmarks/Misc/verified/max_index.rs @@ -16,6 +16,8 @@ pub fn myfun1(x: &Vec) -> (max_index: usize) i <= x.len(), max_index < x.len(), forall|k: int| 0 <= k < i ==> x[max_index as int] >= x[k], + decreases + x.len() - i, { if x[i] > x[max_index] { max_index = i; diff --git a/benchmarks/Misc/verified/remove_all_greater.rs b/benchmarks/Misc/verified/remove_all_greater.rs index 483d05c9..263ab9b0 100644 --- a/benchmarks/Misc/verified/remove_all_greater.rs +++ b/benchmarks/Misc/verified/remove_all_greater.rs @@ -15,6 +15,8 @@ pub fn remove_all_greater(v: Vec, e: i32) -> (result: Vec) invariant forall |k:int| 0 <= k < result.len() ==> result[k] <= e && v@.contains(result[k]), forall |k:int| 0 <= k < i && v[k] <= e ==> result@.contains(v[k]), + decreases + vlen - i, { if (v[i] <= e) { let ghost old_result = result; diff --git a/benchmarks/Misc/verified/remove_all_greater_v2.rs b/benchmarks/Misc/verified/remove_all_greater_v2.rs index 5aee8559..cdd74165 100644 --- a/benchmarks/Misc/verified/remove_all_greater_v2.rs +++ b/benchmarks/Misc/verified/remove_all_greater_v2.rs @@ -25,6 +25,8 @@ pub fn remove_all_greater(v: Vec, e: i32) -> (result: Vec) invariant forall |k:int| 0 <= k < result.len() ==> result[k] <= e && v@.contains(result[k]), forall |k:int| 0 <= k < i && v[k] <= e ==> result@.contains(v[k]), + decreases + v.len() - i, { if (v[i] <= e) { proof{ diff --git a/benchmarks/Misc/verified/simple_nested.rs b/benchmarks/Misc/verified/simple_nested.rs index 18b534fa..9a817ffb 100644 --- a/benchmarks/Misc/verified/simple_nested.rs +++ b/benchmarks/Misc/verified/simple_nested.rs @@ -20,6 +20,8 @@ pub fn simple_nested(a: &mut Vec, b: &Vec, N: i32) -> (sum: i32) b.len() == N, // always specify the length of vectors used in the loop forall |k:int| k <= #[trigger] b[k] <= k + 1, i <= sum <= 2*i, + decreases + N - i, { a.set(i, b[i] + 1); let mut j: usize = 0; diff --git a/benchmarks/Misc/verified/sum.rs b/benchmarks/Misc/verified/sum.rs index dd82b7ec..75e68c8f 100644 --- a/benchmarks/Misc/verified/sum.rs +++ b/benchmarks/Misc/verified/sum.rs @@ -36,6 +36,8 @@ fn compute_arith_sum(n: u64) -> (sum: u64) i <= n, sum == arith_sum_int(i as nat), arith_sum_int(n as nat) < 10000, + decreases + n - i, { i = i + 1; diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/brs1.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/brs1.rs index 51fa6c8c..619a36c5 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/brs1.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/brs1.rs @@ -16,6 +16,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) invariant a.len() == N, forall |k:int| 0 <= k < i ==> a[k] == 1, + decreases + N - i, { if (i % 1 == 0) { a.set(i, 1); @@ -33,6 +35,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) a.len() == N, i > 0 ==> sum[0] <= i, forall |k:int| 0 <= k < N ==> a[k] == 1, + decreases + N - i, { if (i == 0) { sum.set(0, 0); diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/brs2.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/brs2.rs index bcee46b6..cc626f09 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/brs2.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/brs2.rs @@ -16,6 +16,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) invariant forall |k:int| 0<= k < i ==> a[k] == 2 || a[k] == 0, a.len() == N, + decreases + N - i, { if (i % 2 == 0) { a.set(i, 2); @@ -35,6 +37,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) sum.len() == 1, i > 0 ==> sum[0] <= 2 * i, N < 1000, + decreases + N - i, { if (i == 0) { sum.set(0, 0); diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/brs3.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/brs3.rs index 7805313c..a11ffd8a 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/brs3.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/brs3.rs @@ -16,6 +16,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) invariant forall |k: int| 0<= k < i ==> a[k] == 3 || a[k] == 0, a.len() == N, + decreases + N - i, { if (i % 3 == 0) { a.set(i, 3); @@ -35,6 +37,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) sum.len() == 1, i>0 ==> sum[0] <= 3 * i, N < 1000, + decreases + N - i, { if (i == 0) { sum.set(0, 0); diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/brs4.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/brs4.rs index be342b37..c24386b6 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/brs4.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/brs4.rs @@ -16,6 +16,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) invariant forall |k:int| 0<= k < i ==> a[k] == 4 || a[k] == 0, a.len() == N, + decreases + N - i, { if (i % 4 == 0) { a.set(i, 4); @@ -35,6 +37,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) sum.len() == 1, i > 0 ==> sum[0] <= 4 * i, N < 1000, + decreases + N - i, { if (i == 0) { sum.set(0, 0); diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/brs5.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/brs5.rs index b5b7765e..81437f47 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/brs5.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/brs5.rs @@ -16,6 +16,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) invariant forall |k:int| 0<= k < i ==> a[k] == 5 || a[k] == 0, a.len() == N, + decreases + N - i, { if (i % 5 == 0) { a.set(i, 5); @@ -35,6 +37,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) sum.len() == 1, i>0 ==> sum[0] <= 5 * i, N < 1000, + decreases + N - i, { if (i == 0) { sum.set(0, 0); diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/conda.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/conda.rs index 8c2e2d14..592dc9d8 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/conda.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/conda.rs @@ -16,6 +16,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) invariant forall |k:int| 0<= k < i ==> a[k] == 1, a.len() == N, + decreases + N - i, { a.set(i, 1); i = i + 1; @@ -27,6 +29,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) forall |k:int| 0<= k < i ==> a[k] == 2, forall |k:int| i<= k < N ==> a[k] == 1, a.len() == N, + decreases + N - i, { if (a[i] == 1) { a.set(i, a[i] + 1); @@ -45,6 +49,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) sum.len() == 1, a.len() == N, N < 1000, + decreases + N - i, { sum.set(0, sum[0] + a[i]); i = i + 1; diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/condg.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/condg.rs index f4485e6f..23575a70 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/condg.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/condg.rs @@ -15,6 +15,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) invariant forall |k:int| 0 <= k < i ==> a[k] == 1, a.len() == N, + decreases + N - i, { a.set(i, 1); i = i + 1; @@ -28,6 +30,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) a.len() == N, sum[0] == i, sum.len() == 1, + decreases + N - i, { sum.set(0, sum[0] + a[i]); i = i + 1; @@ -41,6 +45,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) a.len() == N, sum.len() == 1, sum[0] == N, + decreases + N - i, { if (sum[0] == N) { a.set(i, a[i] - 1); diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/condm.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/condm.rs index 1a16c894..0e52e02f 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/condm.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/condm.rs @@ -14,6 +14,8 @@ pub fn myfun(a: &mut Vec, N: u32) invariant forall |k:int| 0 <= k < i ==> a[k] == 0, a.len() == N, + decreases + N - i, { a.set(i, 0); i = i + 1; @@ -25,6 +27,8 @@ pub fn myfun(a: &mut Vec, N: u32) forall |k:int| 0 <= k < i ==> a[k] % 2 == N % 2, forall |k:int| i <= k < N ==> a[k] == 0, a.len() == N, + decreases + N - i, { if (N % 2 == 0) { a.set(i, a[i] + 2); diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/condn.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/condn.rs index 5b11b95e..19df1a75 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/condn.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/condn.rs @@ -13,6 +13,8 @@ pub fn myfun(a: &mut Vec, N: i32, m: i32) while (i < N as usize) invariant a.len() == N, + decreases + N - i, { a.set(i, m); i = i + 1; @@ -23,6 +25,8 @@ pub fn myfun(a: &mut Vec, N: i32, m: i32) invariant forall |k:int| 0 <= k < i ==> a[k] <= N, a.len() == N, + decreases + N - i, { if (a[i] < N) { a.set(i, a[i]); diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/ms1.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/ms1.rs index 98ee8d28..5d904c64 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/ms1.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/ms1.rs @@ -15,6 +15,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: usize) invariant forall |k: int| 0<= k < i ==> a[k] == 0, a.len() == N, + decreases + N - i, { a.set(i, i % 1 ); i = i + 1; @@ -28,6 +30,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: usize) a.len() == N, i > 0 ==> sum[0] == 0, sum.len() == 1, + decreases + N - i, { if (i == 0) { sum.set(0, 0); diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/ms2.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/ms2.rs index a74c78b9..2935f806 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/ms2.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/ms2.rs @@ -15,6 +15,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: usize) invariant forall |k:int| 0<= k < i ==> a[k] == 0 || a[k] == 1, a.len() == N, + decreases + N - i, { a.set(i, i % 2 ); i = i + 1; @@ -29,6 +31,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: usize) a.len() == N, sum.len() == 1, i>0 ==> sum[0] <= i, + decreases + N - i, { if (i == 0) { sum.set(0, 0); diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/ms3.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/ms3.rs index b0ac229e..5d95be97 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/ms3.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/ms3.rs @@ -16,6 +16,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) invariant forall |k:int| 0<= k < i ==> a[k] == 0 || a[k] == 1 || a[k] == 2, a.len() == N, + decreases + N - i, { a.set(i, (i % 3) as i32); i = i + 1; @@ -31,6 +33,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) sum.len() == 1, i > 0 ==> sum[0] <= 2 * i, N < 1000, + decreases + N - i, { if (i == 0) { sum.set(0, 0); diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/ms4.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/ms4.rs index ea61e5e5..1b84d8aa 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/ms4.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/ms4.rs @@ -16,6 +16,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) invariant forall |k:int| 0<= k < i ==> a[k] == k % 4, a.len() == N, + decreases + N - i, { a.set(i, (i % 4) as i32); i = i + 1; @@ -31,6 +33,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) forall |k:int| 0<= k < N ==> a[k] == k % 4, a.len() == N, N < 1000, + decreases + N - i, { if (i == 0) { sum.set(0, 0); diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/ms5.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/ms5.rs index 156fd945..f2c934ea 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/ms5.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/ms5.rs @@ -16,6 +16,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) invariant forall |k:int| 0<= k < i ==> a[k] == k % 5, a.len() == N, + decreases + N - i, { a.set(i, (i % 5) as i32); i = i + 1; @@ -31,6 +33,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) i > 0 ==> sum[0] <= 4 * i, sum.len() == 1, N < 1000, + decreases + N - i, { if (i == 0) { sum.set(0, 0); diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/res1.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/res1.rs index 4d1e6edc..fc8e994d 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/res1.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/res1.rs @@ -20,6 +20,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, sum: &mut Vec, N: i32) invariant a.len() == N, forall |k:int| 0 <= k < i ==> a[k] == 1, + decreases + N - i, { a.set(i, 1); i = i + 1; @@ -30,6 +32,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, sum: &mut Vec, N: i32) invariant b.len() == N, forall |k:int| 0 <= k < i ==> b[k] == 1, + decreases + N - i, { b.set(i, 1); i = i + 1; @@ -43,6 +47,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, sum: &mut Vec, N: i32) sum[0] == i, a.len() == N, forall |k:int| 0 <= k < N ==> a[k] == 1, + decreases + N - i, { sum.set(0, sum[0] + a[i]); i = i + 1; @@ -57,6 +63,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, sum: &mut Vec, N: i32) sum[0] == N + i, N < 1000, forall |k:int| 0 <= k < N ==> b[k] == 1, + decreases + N - i, { sum.set(0, sum[0] + b[i]); i = i + 1; diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/res1o.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/res1o.rs index b54a61f6..692ea909 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/res1o.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/res1o.rs @@ -17,6 +17,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, sum: &mut Vec, N: i32) invariant a.len() == N, forall |k:int| 0 <= k < i ==> a[k] == 1, + decreases + N - i, { a.set(i, 1); i = i + 1; @@ -30,6 +32,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, sum: &mut Vec, N: i32) a.len() == N, sum[0] == i, // Corrected invariant forall |k:int| 0 <= k < N ==> a[k] == 1, + decreases + N - i, { sum.set(0, sum[0] + a[i]); i = i + 1; @@ -40,6 +44,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, sum: &mut Vec, N: i32) invariant b.len() == N, forall |k:int| 0 <= k < i ==> b[k] == 1, + decreases + N - i, { b.set(i, 1); i = i + 1; @@ -54,6 +60,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, sum: &mut Vec, N: i32) sum[0] == N + i, forall |k:int| 0 <= k < N ==> b[k] == 1, N < 1000, + decreases + N - i, { sum.set(0, sum[0] + b[i]); i = i + 1; diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/res2.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/res2.rs index d020910c..ab19822c 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/res2.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/res2.rs @@ -20,6 +20,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, c: &mut Vec, sum: &mut Vec invariant a.len() == N, forall |j: int| 0<= j < i ==> a[j] == 1, + decreases + N - i, { a.set(i, 1); i = i + 1; @@ -33,6 +35,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, c: &mut Vec, sum: &mut Vec sum[0] == i, a.len() == N, forall |j: int| 0 <= j < N ==> a[j] == 1, + decreases + N - i, { sum.set(0, sum[0] + a[i]); i = i + 1; @@ -43,6 +47,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, c: &mut Vec, sum: &mut Vec invariant b.len() == N, forall |j: int| 0 <= j < i ==> b[j] == 1, + decreases + N - i, { b.set(i, 1); i = i + 1; @@ -57,6 +63,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, c: &mut Vec, sum: &mut Vec b.len() == N, forall |j: int| 0 <= j < N ==> b[j] == 1, N < 1000, + decreases + N - i, { sum.set(0, sum[0] + b[i]); i = i + 1; @@ -67,6 +75,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, c: &mut Vec, sum: &mut Vec invariant forall |j: int| 0<= j < i ==> c[j] == 1, c.len() == N, + decreases + N - i, { c.set(i, 1); i = i + 1; @@ -81,6 +91,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, c: &mut Vec, sum: &mut Vec forall |j: int| 0 <= j < N ==> c[j] == 1, sum.len() == 1, N < 1000, + decreases + N - i, { sum.set(0, sum[0] + c[i]); i = i + 1; diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/res2o.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/res2o.rs index b24ceab0..f788b21e 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/res2o.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/res2o.rs @@ -19,6 +19,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, c: &mut Vec, sum: &mut Vec invariant forall |j: int| 0<= j < i ==> a[j] == 1, a.len() == N, + decreases + N - i, { a.set(i, 1); i = i + 1; @@ -29,6 +31,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, c: &mut Vec, sum: &mut Vec invariant forall |j: int| 0<= j < i ==> b[j] == 1, b.len() == N, + decreases + N - i, { b.set(i, 1); i = i + 1; @@ -39,6 +43,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, c: &mut Vec, sum: &mut Vec invariant forall |j: int| 0<= j < i ==> c[j] == 1, c.len() == N, + decreases + N - i, { c.set(i, 1); i = i + 1; @@ -52,6 +58,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, c: &mut Vec, sum: &mut Vec sum[0] == i, forall |j: int| 0<= j < N ==> a[j] == 1, a.len() == N, + decreases + N - i, { sum.set(0, sum[0] + a[i]); i = i + 1; @@ -66,6 +74,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, c: &mut Vec, sum: &mut Vec forall |j: int| 0<= j < N ==> b[j] == 1, b.len() == N, N < 1000, + decreases + N - i, { sum.set(0, sum[0] + b[i]); i = i + 1; @@ -80,6 +90,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, c: &mut Vec, sum: &mut Vec forall |j: int| 0<= j < N ==> c[j] == 1, c.len() == N, N < 1000, + decreases + N - i, { sum.set(0, sum[0] + c[i]); i = i + 1; diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/s12if.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/s12if.rs index 87122688..a7c52602 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/s12if.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/s12if.rs @@ -16,6 +16,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: usize) invariant a.len() == N, forall |k:int| 0<= k < i ==> a[k] == 1, + decreases + N - i, { a.set(i, 1); i = i + 1; @@ -27,6 +29,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: usize) a.len() == N, forall |k:int| 0<= k < i ==> a[k] == 2, forall |k:int| i<= k < N ==> a[k] == 1, + decreases + N - i, { if (a[i] == 1) { a.set(i, a[i] + 1); @@ -45,6 +49,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: usize) sum.len() == 1, sum[0] == 2 * i, N < 1000, + decreases + N - i, { if (a[i] == 2) { sum.set(0, sum[0] + a[i]); diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/s1if.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/s1if.rs index c259208a..2e047585 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/s1if.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/s1if.rs @@ -16,6 +16,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) invariant forall |k:int| 0<= k < i ==> a[k] == 1, a.len() == N, + decreases + N - i, { a.set(i, 1); i = i + 1; @@ -29,6 +31,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) a.len() == N, sum[0] == i, sum.len() == 1, + decreases + N - i, { if (a[i] == 1) { sum.set(0, sum[0] + a[i]); diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/s1lif.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/s1lif.rs index 8206738e..6457c8f4 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/s1lif.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/s1lif.rs @@ -16,6 +16,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) invariant a.len() == N, forall |j: int| 0<= j < i ==> a[j] == 1, + decreases + N - i, { a.set(i, 1); i = i + 1; @@ -27,6 +29,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) a.len() == N, forall |j: int| 0<= j < i ==> a[j] == 2, forall |j: int| i<= j < N ==> a[j] == 1, + decreases + N - i, { if (a[i] == 1) { a.set(i, a[i] + 1); @@ -45,6 +49,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) sum.len() == 1, sum[0] == 2 * i, N < 1000, + decreases + N - i, { sum.set(0, sum[0] + a[i]); i = i + 1; diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/s22if.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/s22if.rs index 6fbe9765..46d21130 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/s22if.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/s22if.rs @@ -16,6 +16,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: usize) invariant a.len() == N, forall |k:int| 0<= k < i ==> a[k] == 1, + decreases + N - i, { a.set(i, 1); i = i + 1; @@ -27,6 +29,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: usize) a.len() == N, forall |k:int| 0<= k < i ==> a[k] == 3, forall |k:int| i<= k < N ==> a[k] == 1, + decreases + N - i, { if (a[i] == 1) { a.set(i, a[i] + 2); @@ -45,6 +49,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: usize) sum.len() == 1, sum[0] == 3 * i, N < 1000, + decreases + N - i, { if (a[i] == 3) { sum.set(0, sum[0] + a[i]); diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/s2if.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/s2if.rs index 8792e7ae..5113f45c 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/s2if.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/s2if.rs @@ -16,6 +16,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) invariant forall |k:int| 0<= k < i ==> a[k] == 2, a.len() == N, + decreases + N - i, { a.set(i, 2); i = i + 1; @@ -30,6 +32,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) sum[0] == 2 * i, sum.len() == 1, N < 1000, + decreases + N - i, { if (a[i] == 2) { sum.set(0, sum[0] + a[i]); diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/s2lif.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/s2lif.rs index ad20a1eb..f1584258 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/s2lif.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/s2lif.rs @@ -16,6 +16,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) invariant forall |j: int| 0<= j < i ==> a[j] == 1, a.len() == N, + decreases + N - i, { a.set(i, 1); i = i + 1; @@ -27,6 +29,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) forall |j: int| 0<= j < i ==> a[j] == 3, forall |j: int| i <= j < N ==> a[j] == 1, a.len() == N, + decreases + N - i, { if (a[i] == 1) { a.set(i, a[i] + 2); @@ -45,6 +49,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) sum[0] == 3 * i, N <= 1000, a.len() == N, + decreases + N - i, { sum.set(0, sum[0] + a[i]); i = i + 1; diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/s32if.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/s32if.rs index e77ad8d4..bac742b9 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/s32if.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/s32if.rs @@ -16,6 +16,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: usize) invariant forall |k:int| 0<=k a[k] == 1, a.len() == N, + decreases + N - i, { a.set(i, 1); i = i + 1; @@ -27,6 +29,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: usize) forall |k:int| 0<=k a[k] == 4, forall |k:int| i<=k a[k] == 1, a.len() == N, + decreases + N - i, { if (a[i] == 1) { a.set(i, a[i] + 3); @@ -45,6 +49,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: usize) sum[0] == 4 * i, sum.len() == 1, N < 1000, + decreases + N - i, { if (a[i] == 4) { sum.set(0, sum[0] + a[i]); diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/s3if.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/s3if.rs index 95eea2bf..d6eb61aa 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/s3if.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/s3if.rs @@ -17,6 +17,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) invariant forall |k:int| 0<= k < i ==> a[k] == 3, a.len() == N, + decreases + N - i, { a.set(i, 3); i = i + 1; @@ -31,6 +33,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) sum[0] == 3 * i, sum.len() == 1, N < 1000, + decreases + N - i, { if (a[i] == 3) { sum.set(0, sum[0] + a[i]); diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/s3lif.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/s3lif.rs index e912a14a..6a2de62f 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/s3lif.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/s3lif.rs @@ -16,6 +16,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) invariant forall |j: int| 0<= j < i ==> a[j] == 1, a.len() == N, + decreases + N - i, { a.set(i, 1); i = i + 1; @@ -27,6 +29,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) forall |j: int| 0<= j < i ==> a[j] == 4, forall |j: int| i <= j < N ==> a[j] == 1, a.len() == N, + decreases + N - i, { if (a[i] == 1) { a.set(i, a[i] + 3); @@ -45,6 +49,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) sum.len() == 1, sum[0] == 4 * i, N <= 1000, + decreases + N - i, { sum.set(0, sum[0] + a[i]); i = i + 1; diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/s42if.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/s42if.rs index a397d2c1..80f1a28e 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/s42if.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/s42if.rs @@ -16,6 +16,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: usize) invariant forall |k:int| 0<= k < i ==> a[k] == 1, a.len() == N, + decreases + N - i, { a.set(i, 1); i = i + 1; @@ -27,6 +29,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: usize) forall |k:int| 0<= k < i ==> a[k] == 5, forall |k:int| i<= k < N ==> a[k] == 1, a.len() == N, + decreases + N - i, { if (a[i] == 1) { a.set(i, a[i] + 4); @@ -45,6 +49,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: usize) sum[0] == 5 * i, sum.len() == 1, N < 1000, + decreases + N - i, { if (a[i] == 5) { diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/s4if.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/s4if.rs index d750adb9..48ce1587 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/s4if.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/s4if.rs @@ -16,6 +16,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) invariant forall |k:int| 0<= k < i ==> a[k] == 4, a.len() == N, + decreases + N - i, { a.set(i, 4); i = i + 1; @@ -30,6 +32,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) sum[0] == 4 * i, sum.len() == 1, N < 1000, + decreases + N - i, { if (a[i] == 4) { sum.set(0, sum[0] + a[i]); diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/s4lif.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/s4lif.rs index bd3bedaf..4e19a3ac 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/s4lif.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/s4lif.rs @@ -17,6 +17,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) invariant a.len() == N, forall |j: int| 0<= j < i ==> a[j] == 1, + decreases + N - i, { a.set(i, 1); i = i + 1; @@ -28,6 +30,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) a.len() == N, forall |j: int| 0<= j < i ==> a[j] == 5, forall |j: int| i <= j < N ==> a[j] == 1, + decreases + N - i, { if (a[i] == 1) { a.set(i, a[i] + 4); @@ -46,6 +50,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) forall |j: int| 0<= j < N ==> a[j] == 5, sum[0] == 5 * i, N < 1000, + decreases + N - i, { sum.set(0, sum[0] + a[i]); i = i + 1; diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/s52if.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/s52if.rs index 04e38a89..5f51565c 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/s52if.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/s52if.rs @@ -17,6 +17,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: usize) invariant forall |k:int| 0 <= k < i ==> a[k] == 1, a.len() == N, + decreases + N - i, { a.set(i, 1); i = i + 1; @@ -28,6 +30,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: usize) forall |k:int| 0 <= k < i ==> a[k] == 6, forall |k:int| i <= k < N ==> a[k] == 1, a.len() == N, + decreases + N - i, { if (a[i] == 1) { a.set(i, a[i] + 5); @@ -46,6 +50,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: usize) sum[0] == 6 * i, sum.len() == 1, N < 1000, + decreases + N - i, { if (a[i] == 6) { diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/s5if.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/s5if.rs index 164967fa..ea908bf4 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/s5if.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/s5if.rs @@ -17,6 +17,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) invariant forall |k:int| 0<= k < i ==> a[k] == 5, a.len() == N, + decreases + N - i, { a.set(i, 5); i = i + 1; @@ -31,6 +33,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) sum[0] == 5 * i, sum.len() == 1, N < 1000, + decreases + N - i, { if (a[i] == 5) { sum.set(0, sum[0] + a[i]); diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/s5lif.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/s5lif.rs index b89f7a48..3179b2ff 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/s5lif.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/s5lif.rs @@ -17,6 +17,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) invariant forall |j: int| 0<= j < i ==> a[j] == 1, a.len() == N, + decreases + N - i, { a.set(i, 1); i = i + 1; @@ -28,6 +30,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) forall |j: int| 0<= j < i ==> a[j] == 6, forall |j: int| i <= j < N ==> a[j] == 1, a.len() == N, + decreases + N - i, { if (a[i] == 1) { a.set(i, a[i] + 5); @@ -46,6 +50,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) sum.len() == 1, a.len() == N, N < 1000, + decreases + N - i, { sum.set(0, sum[0] + a[i]); i = i + 1; diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/sina1.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/sina1.rs index c1dc0022..c6ed9ab9 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/sina1.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/sina1.rs @@ -17,6 +17,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) i <= N, sum.len() == 1, sum[0] == i, + decreases + N - i, { sum.set(0, sum[0] + 1); i = i + 1; @@ -28,6 +30,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) forall |k:int| 0 <= k < i ==> a[k] == sum[0], sum.len() == 1, a.len() == N, + decreases + N - i, { a.set(i, sum[0]); i = i + 1; diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/sina2.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/sina2.rs index 368d801d..57722c89 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/sina2.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/sina2.rs @@ -17,6 +17,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) invariant forall |k:int| 0 <= k < i ==> a[k] == 1, a.len() == N, + decreases + N - i, { a.set(i, 1); i = i + 1; @@ -30,6 +32,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) sum[0] == i, a.len() == N, sum.len() == 1, + decreases + N - i, { sum.set(0, sum[0] + a[i]); i = i + 1; @@ -44,6 +48,8 @@ pub fn myfun(a: &mut Vec, sum: &mut Vec, N: i32) a.len() == N, sum.len() == 1, N < 1000, + decreases + N - i, { a.set(i, a[i] + sum[0]); i = i + 1; diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/sina3.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/sina3.rs index ecde647c..a102acd2 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/sina3.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/sina3.rs @@ -17,6 +17,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, sum: &mut Vec, N: i32) invariant forall |k:int| 0 <= k < i ==> a[k] == 1, a.len() == N, + decreases + N - i, { a.set(i, 1); i = i + 1; @@ -27,6 +29,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, sum: &mut Vec, N: i32) invariant forall |k:int| 0 <= k < i ==> b[k] == 1, b.len() == N, + decreases + N - i, { b.set(i, 1); i = i + 1; @@ -40,6 +44,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, sum: &mut Vec, N: i32) forall |k:int| 0 <= k < N ==> a[k] == 1, a.len() == N, sum[0] == i, + decreases + N - i, { sum.set(0, sum[0] + a[i]); i = i + 1; @@ -55,6 +61,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, sum: &mut Vec, N: i32) sum.len() == 1, sum[0] == N, N < 1000, + decreases + N - i, { a.set(i, b[i] + sum[0]); i = i + 1; diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/sina4.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/sina4.rs index b7c6ce3e..69acc33f 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/sina4.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/sina4.rs @@ -17,6 +17,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, sum: &mut Vec, N: i32) invariant forall |k:int| 0 <= k < i ==> a[k] == 1, a.len() == N, + decreases + N - i, { a.set(i, 1); i = i + 1; @@ -30,6 +32,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, sum: &mut Vec, N: i32) a.len() == N, sum[0] == i, sum.len() == 1, + decreases + N - i, { sum.set(0, sum[0] + a[i]); i = i + 1; @@ -44,6 +48,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, sum: &mut Vec, N: i32) forall |k:int| 0 <= k < i ==> a[k] == N + 1, a.len() == N, N < 1000, + decreases + N - i, { a.set(i, a[i] + sum[0]); i = i + 1; @@ -57,6 +63,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, sum: &mut Vec, N: i32) forall |k:int| 0 <= k < i ==> b[k] == N + 2, b.len() == N, N < 1000, + decreases + N - i, { b.set(i, a[i] + 1); i = i + 1; diff --git a/benchmarks/SVComp-Array-fpi-nonl/verified/sina5.rs b/benchmarks/SVComp-Array-fpi-nonl/verified/sina5.rs index b38746a8..8c3be83e 100644 --- a/benchmarks/SVComp-Array-fpi-nonl/verified/sina5.rs +++ b/benchmarks/SVComp-Array-fpi-nonl/verified/sina5.rs @@ -18,6 +18,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, sum: &mut Vec, N: i32) invariant forall |k:int| 0 <= k < i ==> a[k] == 1, a.len() == N, + decreases + N - i, { a.set(i, 1); i = i + 1; @@ -28,6 +30,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, sum: &mut Vec, N: i32) invariant forall |k:int| 0 <= k < i ==> b[k] == 1, b.len() == N, + decreases + N - i, { b.set(i, 1); i = i + 1; @@ -41,6 +45,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, sum: &mut Vec, N: i32) forall |k:int| 0 <= k < N ==> a[k] == 1, a.len() == N, sum[0] == i, + decreases + N - i, { sum.set(0, sum[0] + a[i]); i = i + 1; @@ -55,6 +61,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, sum: &mut Vec, N: i32) sum[0] == N + i, sum.len() == 1, N < 1000, + decreases + N - i, { sum.set(0, sum[0] + b[i]); i = i + 1; @@ -68,6 +76,8 @@ pub fn myfun(a: &mut Vec, b: &mut Vec, sum: &mut Vec, N: i32) a.len() == N, sum[0] == 2 * N, sum.len() == 1, + decreases + N - i, { a.set(i, a[i] + sum[0]); i = i + 1;