Fresh copy let var initializer.

This is safe becaues it consumes whatever is the initializer.

stainless_extraction/src/expr/block.rs

@@ -124,8 +124,12 @@ impl<'a, 'l, 'tcx> BodyExtractor<'a, 'l, 'tcx> {
                 let exprs = acc_exprs.clone();
                 acc_exprs.clear();
                 let body_expr = self.extract_block_(stmts, acc_exprs, acc_specs, final_expr);
+
                 // wrap that body expression into the Let
-                let init = self.extract_expr(init);
+
+                // This is safe, because we don't support mutable references.
+                let init = self.extract_aliasable_expr(init);
+
                 let last_expr = if vd.is_mutable() {
                   f.LetVar(vd, init, body_expr).into()
                 } else {

stainless_frontend/tests/pass/mut_local_lets.rs

@@ -2,9 +2,22 @@
 
 extern crate stainless;
 
-pub enum IntOption {
-  None,
-  Some(i32),
+pub fn f<T>(option: Option<T>) {
+  // Again, local mutation
+  let mut option2 = None;
+  let mut option = None;
+  option2 = option;
+  option = Some(123);
+}
+
+pub struct Thing<T> {
+  field: T,
+}
+
+pub fn change_thing<T>(thing: Thing<T>, t: T) -> Thing<T> {
+  let mut new_field = thing.field;
+  new_field = t;
+  Thing { field: new_field }
 }
 
 pub fn main() {
@@ -13,11 +26,4 @@ pub fn main() {
   assert!(x == 1);
   x = 3;
   assert!(x == 3);
-
-  // Again, local mutation
-  let option = IntOption::Some(2);
-  let mut option2 = IntOption::None;
-  let mut option = IntOption::None;
-  option2 = option;
-  option = IntOption::Some(123);
 }