Add decreases clauses for loops

benchmarks/MBPP/verified/task_id_105.rs

@@ -37,6 +37,8 @@ fn count_true(arr: &Vec<bool>) -> (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;

benchmarks/MBPP/verified/task_id_113.rs

@@ -30,6 +30,8 @@ fn is_integer(text: &Vec<char>) -> (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;

benchmarks/MBPP/verified/task_id_133.rs

@@ -42,6 +42,8 @@ fn sum_negatives(arr: &Vec<i64>) -> (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);

benchmarks/MBPP/verified/task_id_142.rs

@@ -65,6 +65,8 @@ fn count_identical_position(arr1: &Vec<i32>, arr2: &Vec<i32>, arr3: &Vec<i32>) -
                 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;

benchmarks/MBPP/verified/task_id_145.rs

@@ -28,6 +28,8 @@ fn max_difference(arr: &Vec<i32>) -> (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];

benchmarks/MBPP/verified/task_id_161.rs

@@ -36,6 +36,9 @@ fn contains(str: &Vec<i32>, 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<i32>, arr2: &Vec<i32>) -> (result: Vec<i32>)
                 0 <= k < index ==> (arr2@.contains(#[trigger] arr1[k]) || output_str@.contains(
                     #[trigger] arr1[k],
                 )),
+    decreases
+        arr1.len() - index,
     {
         if (!contains(arr2, arr1[index])) {
             proof {

benchmarks/MBPP/verified/task_id_170.rs

@@ -49,6 +49,8 @@ fn sum_range_list(arr: &Vec<i64>, 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,

benchmarks/MBPP/verified/task_id_18.rs

@@ -51,6 +51,8 @@ fn contains(str: &Vec<char>, 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<char>, str2: &Vec<char>) -> (result: Vec<char>)
                 0 <= k < index ==> (str2@.contains(#[trigger] str1[k]) || output_str@.contains(
                     #[trigger] str1[k],
                 )),
+        decreases
+            str1.len() - index,
     {
         if (!contains(str2, str1[index])) {
             proof {

benchmarks/MBPP/verified/task_id_2.rs

@@ -27,6 +27,8 @@ fn contains(arr: &Vec<i32>, 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<i32>, list2: &Vec<i32>) -> (shared: Vec<i32>)
                     #[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]);

benchmarks/MBPP/verified/task_id_230.rs

@@ -47,6 +47,8 @@ fn replace_blanks_with_chars(str1: &Vec<char>, ch: char) -> (result: Vec<char>)
                 } else {
                     str1[k]
                 }),
+        decreases
+            str1.len() - index, 
     {
         if (str1[index] == ' ') {
             out_str.push(ch);

benchmarks/MBPP/verified/task_id_240.rs

@@ -34,6 +34,8 @@ fn replace_last_element(first: &Vec<i32>, second: &Vec<i32>) -> (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<i32>, second: &Vec<i32>) -> (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;

benchmarks/MBPP/verified/task_id_249.rs

@@ -27,6 +27,9 @@ fn contains(arr: &Vec<i32>, 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<i32>, arr2: &Vec<i32>) -> (result: Vec<i32>)
                 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]);

benchmarks/MBPP/verified/task_id_251.rs

@@ -35,6 +35,8 @@ fn insert_before_each(arr: &Vec<i32>, elem: i32) -> (result: Vec<i32>)
             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]);

benchmarks/MBPP/verified/task_id_261.rs

@@ -46,6 +46,8 @@ fn element_wise_division(arr1: &Vec<u32>, arr2: &Vec<u32>) -> (result: Vec<u32>)
                     <= 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;

benchmarks/MBPP/verified/task_id_262.rs

@@ -34,6 +34,8 @@ fn split_array(list: &Vec<i32>, l: usize) -> (new_list: (Vec<i32>, Vec<i32>))
             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<i32>, l: usize) -> (new_list: (Vec<i32>, Vec<i32>))
         invariant
             l <= index <= list.len(),
             part2@ =~= list@.subrange(l as int, index as int),
+        decreases
+            list.len() - index,
     {
         part2.push(list[index]);
         index += 1;

benchmarks/MBPP/verified/task_id_273.rs

@@ -40,6 +40,8 @@ fn element_wise_subtract(arr1: &Vec<i32>, arr2: &Vec<i32>) -> (result: Vec<i32>)
                 (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;

benchmarks/MBPP/verified/task_id_282.rs

@@ -38,6 +38,9 @@ fn element_wise_subtract(arr1: &Vec<i32>, arr2: &Vec<i32>) -> (result: Vec<i32>)
                 (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;

benchmarks/MBPP/verified/task_id_284.rs

@@ -19,6 +19,8 @@ fn all_elements_equals(arr: &Vec<i32>, 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;

benchmarks/MBPP/verified/task_id_290.rs

@@ -43,6 +43,8 @@ fn max_length_list(seq: &Vec<Vec<i32>>) -> (max_list: &Vec<i32>)
             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];

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

benchmarks/MBPP/verified/task_id_307.rs

@@ -25,6 +25,8 @@ fn list_deep_clone(arr: &Vec<u64>) -> (copied: Vec<u64>)
             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;

benchmarks/MBPP/verified/task_id_399.rs

@@ -36,6 +36,8 @@ fn bit_wise_xor(arr1: &Vec<i32>, arr2: &Vec<i32>) -> (result: Vec<i32>)
             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;

benchmarks/MBPP/verified/task_id_412.rs

@@ -23,6 +23,8 @@ fn remove_odds(arr: &Vec<u32>) -> (even_list: Vec<u32>)
         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]);

benchmarks/MBPP/verified/task_id_414.rs

@@ -19,6 +19,8 @@ fn contains(arr: &Vec<i32>, 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<i32>, arr2: &Vec<i32>) -> (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;

benchmarks/MBPP/verified/task_id_424.rs

@@ -52,6 +52,8 @@ fn extract_rear_chars(s: &Vec<Vec<char>>) -> (result: Vec<char>)
             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]);

benchmarks/MBPP/verified/task_id_426.rs

@@ -29,6 +29,8 @@ fn filter_odd_numbers(arr: &Vec<u32>) -> (odd_list: Vec<u32>)
         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]);

benchmarks/MBPP/verified/task_id_431.rs

@@ -23,13 +23,17 @@ fn has_common_element(list1: &Vec<i32>, list2: &Vec<i32>) -> (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()
             invariant
                 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;

benchmarks/MBPP/verified/task_id_433.rs

@@ -19,6 +19,8 @@ fn is_greater(arr: &Vec<i32>, 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;

benchmarks/MBPP/verified/task_id_436.rs

@@ -23,6 +23,8 @@ fn find_negative_numbers(arr: &Vec<i32>) -> (negative_list: Vec<i32>)
         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]);

benchmarks/MBPP/verified/task_id_445.rs

@@ -49,6 +49,8 @@ fn element_wise_multiplication(arr1: &Vec<i32>, arr2: &Vec<i32>) -> (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;

benchmarks/MBPP/verified/task_id_447.rs

@@ -39,6 +39,8 @@ fn cube_element(nums: &Vec<i32>) -> (cubed: Vec<i32>)
                     * #[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;

benchmarks/MBPP/verified/task_id_454.rs

@@ -19,6 +19,8 @@ fn contains_z(text: &Vec<char>) -> (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;

benchmarks/MBPP/verified/task_id_457.rs

@@ -35,6 +35,8 @@ fn min_sublist(seq: &Vec<Vec<i32>>) -> (min_list: &Vec<i32>)
             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];

benchmarks/MBPP/verified/task_id_460.rs

@@ -28,6 +28,8 @@ fn get_first_elements(arr: &Vec<Vec<i32>>) -> (result: Vec<i32>)
             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);

benchmarks/MBPP/verified/task_id_461.rs

@@ -45,6 +45,8 @@ fn count_uppercase(text: &Vec<char>) -> (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;

benchmarks/MBPP/verified/task_id_472.rs

@@ -24,6 +24,8 @@ fn contains_consecutive_numbers(arr: &Vec<i32>) -> (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;