Fix the bug of using multiple hidden variables for the prev of the same Expr

library/kani_macros/src/sysroot/loop_contracts/mod.rs

@@ -136,9 +136,15 @@ impl VisitMut for CallReplacer {
         if let Expr::Call(call) = expr {
             if let Expr::Path(expr_path) = &*call.func {
                 if self.should_replace(expr_path) {
-                    let new_var = self.generate_var_name();
-                    self.replacements.push((expr.clone(), new_var.clone()));
-                    *expr = syn::parse_quote!(#new_var);
+                    let replace_var =
+                        self.replacements.iter().find(|(e, _)| e == expr).map(|(_, v)| v);
+                    if let Some(var) = replace_var {
+                        *expr = syn::parse_quote!(#var);
+                    } else {
+                        let new_var = self.generate_var_name();
+                        self.replacements.push((expr.clone(), new_var.clone()));
+                        *expr = syn::parse_quote!(#new_var);
+                    };
                 }
             }
         }

tests/expected/loop-contract/multiple_prev.expected

@@ -0,0 +1,9 @@
+func::{closure#3}::{closure#0}::{closure#1}.assertion.1\
+	 - Status: SUCCESS\
+	 - Description: "attempt to add with overflow"
+
+func.loop_invariant_step.1\
+	 - Status: SUCCESS\
+	 - Description: "Check invariant after step for loop func.0"
+
+VERIFICATION:- SUCCESSFUL

tests/expected/loop-contract/multiple_prev.rs

@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z loop-contracts -Z function-contracts
+
+#![feature(proc_macro_hygiene)]
+#![feature(stmt_expr_attributes)]
+
+#[kani::requires(x < 10)]
+fn func(x: usize) -> Option<usize> {
+    let mut i: usize = 0;
+    let mut r: usize = x;
+    let N: usize = 7;
+    #[kani::loop_invariant((i <= N && i >=0) && (on_entry(i) == 0 && prev(i) < 7 && prev(i) + 1 == i )  ) ]
+    while i < N {
+        i = i + 1;
+    }
+    if r + i >= x + N { Some(r) } else { None }
+}
+
+#[kani::proof]
+fn harness() {
+    let a = kani::any_where(|x: &usize| *x < 10);
+    kani::assert(func(a).is_some(), "func(a) is some");
+}