Attempt to fix double return bug.

engine/lib/phases/phase_and_mut_defsite.ml

@@ -116,9 +116,16 @@ struct
           match e.e with
           | GlobalVar (`TupleCons 0) -> e
           | _ ->
-              let lhs = UB.make_var_pat var e.typ e.span in
               let rhs = e in
-              let body = { e with e = LocalVar var } in
+              let lhs, body =
+                if [%eq: ty] e.typ UB.unit_typ then
+                  (* This case has been added to fix https://github.com/hacspec/hax/issues/720.
+                     It might need a better solution. *)
+                  ( UB.M.pat_PWild ~span:e.span ~typ:e.typ,
+                    UB.M.expr_unit ~span:e.span )
+                else
+                  (UB.make_var_pat var e.typ e.span, { e with e = LocalVar var })
+              in
               { body with e = Let { monadic = None; lhs; rhs; body } }
         in
         UB.map_body_of_nested_lets f e

test-harness/src/snapshots/toolchain__attributes into-fstar.snap

@@ -419,7 +419,7 @@ let impl: t_Foo Prims.unit =
     f_i
     =
     fun (x: u8) (y: u8) ->
-      let hax_temp_output:Prims.unit = () <: Prims.unit in
+      let _:Prims.unit = () <: Prims.unit in
       y
   }
 '''

test-harness/src/snapshots/toolchain__loops into-fstar.snap

@@ -27,6 +27,32 @@ stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'
 diagnostics = []
 
 [stdout.files]
+"Loops.And_mut_side_effect_loop.fst" = '''
+module Loops.And_mut_side_effect_loop
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let looping (array: t_Array u8 (sz 5)) : t_Array u8 (sz 5) =
+  let array:t_Array u8 (sz 5) =
+    Rust_primitives.Hax.Folds.fold_range (sz 0)
+      (Core.Slice.impl__len #u8 (array <: t_Slice u8) <: usize)
+      (fun array temp_1_ ->
+          let array:t_Array u8 (sz 5) = array in
+          let _:usize = temp_1_ in
+          true)
+      array
+      (fun array i ->
+          let array:t_Array u8 (sz 5) = array in
+          let i:usize = i in
+          Rust_primitives.Hax.Monomorphized_update_at.update_at_usize array
+            i
+            (cast (i <: usize) <: u8)
+          <:
+          t_Array u8 (sz 5))
+  in
+  array
+'''
 "Loops.Control_flow.fst" = '''
 module Loops.Control_flow
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"

tests/loops/src/lib.rs

@@ -244,3 +244,12 @@ mod control_flow {
         sum
     }
 }
+
+mod and_mut_side_effect_loop {
+    // https://github.com/hacspec/hax/issues/720
+    fn looping(array: &mut [u8; 5]) {
+        for i in 0..array.len() {
+            array[i] = i as u8;
+        }
+    }
+}