diff --git a/engine/lib/phases/phase_and_mut_defsite.ml b/engine/lib/phases/phase_and_mut_defsite.ml
index d640ef92e..78898a425 100644
--- a/engine/lib/phases/phase_and_mut_defsite.ml
+++ b/engine/lib/phases/phase_and_mut_defsite.ml
@@ -95,12 +95,14 @@ struct
       (* visit an expression and replace all `Return e` nodes by `Return (f e)` *)
       let map_returns ~(f : expr -> expr) : expr -> expr =
         let visitor =
-          object
+          object (self)
             inherit [_] Visitors.map as super
 
             method! visit_expr' () e =
               match e with
-              | Return { e; witness } -> Return { e = f e; witness }
+              | Return { e; witness } ->
+                  let e = self#visit_expr () e in
+                  Return { e = f e; witness }
               | _ -> super#visit_expr' () e
           end
         in
diff --git a/engine/lib/side_effect_utils.ml b/engine/lib/side_effect_utils.ml
index 801a3b268..8d3a6b2a6 100644
--- a/engine/lib/side_effect_utils.ml
+++ b/engine/lib/side_effect_utils.ml
@@ -42,9 +42,9 @@ struct
                {
                  details =
                    "Expected two exact same types, got x="
-                   ^ [%show: ty] x
+                   ^ (x |> U.LiftToFullAst.ty |> Print_rust.pty_str)
                    ^ " and y="
-                   ^ [%show: ty] y;
+                   ^ (y |> U.LiftToFullAst.ty |> Print_rust.pty_str);
                })
         else x
       in
diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
index 66c41f5fa..14648c368 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap	
@@ -81,6 +81,31 @@ let test (x y: Core.Option.t_Option i32) : Core.Option.t_Option i32 =
   | Core.Option.Option_Some some -> some
   | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option i32
 '''
+"Side_effects.Nested_return.fst" = '''
+module Side_effects.Nested_return
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let other_fun (rng: i8) : (i8 & Core.Result.t_Result Prims.unit Prims.unit) =
+  let hax_temp_output:Core.Result.t_Result Prims.unit Prims.unit =
+    Core.Result.Result_Ok (() <: Prims.unit) <: Core.Result.t_Result Prims.unit Prims.unit
+  in
+  rng, hax_temp_output <: (i8 & Core.Result.t_Result Prims.unit Prims.unit)
+
+let v_fun (rng: i8) : (i8 & Core.Result.t_Result Prims.unit Prims.unit) =
+  let tmp0, out:(i8 & Core.Result.t_Result Prims.unit Prims.unit) = other_fun rng in
+  let rng:i8 = tmp0 in
+  match out <: Core.Result.t_Result Prims.unit Prims.unit with
+  | Core.Result.Result_Ok hoist6 ->
+    rng, (Core.Result.Result_Ok hoist6 <: Core.Result.t_Result Prims.unit Prims.unit)
+    <:
+    (i8 & Core.Result.t_Result Prims.unit Prims.unit)
+  | Core.Result.Result_Err err ->
+    rng, (Core.Result.Result_Err err <: Core.Result.t_Result Prims.unit Prims.unit)
+    <:
+    (i8 & Core.Result.t_Result Prims.unit Prims.unit)
+'''
 "Side_effects.fst" = '''
 module Side_effects
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -208,7 +233,7 @@ let direct_result_question_mark (y: Core.Result.t_Result Prims.unit u32)
 let direct_result_question_mark_coercion (y: Core.Result.t_Result i8 u16)
     : Core.Result.t_Result i8 u32 =
   match y <: Core.Result.t_Result i8 u16 with
-  | Core.Result.Result_Ok hoist5 -> Core.Result.Result_Ok hoist5 <: Core.Result.t_Result i8 u32
+  | Core.Result.Result_Ok hoist10 -> Core.Result.Result_Ok hoist10 <: Core.Result.t_Result i8 u32
   | Core.Result.Result_Err err ->
     Core.Result.Result_Err (Core.Convert.f_from #u32 #u16 #FStar.Tactics.Typeclasses.solve err)
     <:
@@ -224,12 +249,12 @@ let early_returns (x: u32) : u32 =
       match true <: bool with
       | true -> 34ul
       | _ ->
-        let x, hoist9:(u32 & u32) = x, 3ul <: (u32 & u32) in
-        Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist9 <: u32) x
+        let x, hoist14:(u32 & u32) = x, 3ul <: (u32 & u32) in
+        Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist14 <: u32) x
     else
       let x:u32 = x +! 9ul in
-      let x, hoist9:(u32 & u32) = x, x +! 1ul <: (u32 & u32) in
-      Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist9 <: u32) x
+      let x, hoist14:(u32 & u32) = x, x +! 1ul <: (u32 & u32) in
+      Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist14 <: u32) x
 
 /// Exercise local mutation with control flow and loops
 let local_mutation (x: u32) : u32 =
@@ -257,7 +282,7 @@ let local_mutation (x: u32) : u32 =
     in
     Core.Num.impl__u32__wrapping_add x y
   else
-    let (x, y), hoist19:((u32 & u32) & u32) =
+    let (x, y), hoist24:((u32 & u32) & u32) =
       match x <: u32 with
       | 12ul ->
         let y:u32 = Core.Num.impl__u32__wrapping_add x y in
@@ -269,7 +294,7 @@ let local_mutation (x: u32) : u32 =
         ((u32 & u32) & u32)
       | _ -> (x, y <: (u32 & u32)), 0ul <: ((u32 & u32) & u32)
     in
-    let x:u32 = hoist19 in
+    let x:u32 = hoist24 in
     Core.Num.impl__u32__wrapping_add x y
 
 /// Combine `?` and early return
@@ -277,39 +302,39 @@ let monad_lifting (x: u8) : Core.Result.t_Result t_A t_B =
   if x >. 123uy
   then
     match Core.Result.Result_Err (B <: t_B) <: Core.Result.t_Result t_A t_B with
-    | Core.Result.Result_Ok hoist20 -> Core.Result.Result_Ok hoist20 <: Core.Result.t_Result t_A t_B
+    | Core.Result.Result_Ok hoist25 -> Core.Result.Result_Ok hoist25 <: Core.Result.t_Result t_A t_B
     | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result t_A t_B
   else Core.Result.Result_Ok (A <: t_A) <: Core.Result.t_Result t_A t_B
 
 /// Test question mark on `Option`s with some control flow
 let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.Option.t_Option u8 =
   match x <: Core.Option.t_Option u8 with
-  | Core.Option.Option_Some hoist26 ->
-    if hoist26 >. 10uy
+  | Core.Option.Option_Some hoist31 ->
+    if hoist31 >. 10uy
     then
       match x <: Core.Option.t_Option u8 with
-      | Core.Option.Option_Some hoist28 ->
+      | Core.Option.Option_Some hoist33 ->
         (match
-            Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist28 3uy)
+            Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist33 3uy)
             <:
             Core.Option.t_Option u8
           with
-          | Core.Option.Option_Some hoist34 ->
-            (match hoist34 <: u8 with
+          | Core.Option.Option_Some hoist39 ->
+            (match hoist39 <: u8 with
               | 3uy ->
                 (match Core.Option.Option_None <: Core.Option.t_Option u8 with
                   | Core.Option.Option_Some some ->
                     let v:u8 = some in
                     (match x <: Core.Option.t_Option u8 with
-                      | Core.Option.Option_Some hoist35 ->
+                      | Core.Option.Option_Some hoist40 ->
                         (match y <: Core.Option.t_Option u8 with
-                          | Core.Option.Option_Some hoist36 ->
+                          | Core.Option.Option_Some hoist41 ->
                             Core.Option.Option_Some
                             (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
-                                    hoist35
+                                    hoist40
                                   <:
                                   u8)
-                                hoist36)
+                                hoist41)
                             <:
                             Core.Option.t_Option u8
                           | Core.Option.Option_None  ->
@@ -319,18 +344,18 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
                   | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option u8)
               | 4uy ->
                 (match z <: Core.Option.t_Option u64 with
-                  | Core.Option.Option_Some hoist23 ->
-                    let v:u8 = 4uy +! (if hoist23 >. 4uL <: bool then 0uy else 3uy) in
+                  | Core.Option.Option_Some hoist28 ->
+                    let v:u8 = 4uy +! (if hoist28 >. 4uL <: bool then 0uy else 3uy) in
                     (match x <: Core.Option.t_Option u8 with
-                      | Core.Option.Option_Some hoist35 ->
+                      | Core.Option.Option_Some hoist40 ->
                         (match y <: Core.Option.t_Option u8 with
-                          | Core.Option.Option_Some hoist36 ->
+                          | Core.Option.Option_Some hoist41 ->
                             Core.Option.Option_Some
                             (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
-                                    hoist35
+                                    hoist40
                                   <:
                                   u8)
-                                hoist36)
+                                hoist41)
                             <:
                             Core.Option.t_Option u8
                           | Core.Option.Option_None  ->
@@ -341,14 +366,14 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
               | _ ->
                 let v:u8 = 12uy in
                 match x <: Core.Option.t_Option u8 with
-                | Core.Option.Option_Some hoist35 ->
+                | Core.Option.Option_Some hoist40 ->
                   (match y <: Core.Option.t_Option u8 with
-                    | Core.Option.Option_Some hoist36 ->
+                    | Core.Option.Option_Some hoist41 ->
                       Core.Option.Option_Some
-                      (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v hoist35
+                      (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v hoist40
                             <:
                             u8)
-                          hoist36)
+                          hoist41)
                       <:
                       Core.Option.t_Option u8
                     | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option u8
@@ -358,30 +383,30 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
       | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option u8
     else
       (match x <: Core.Option.t_Option u8 with
-        | Core.Option.Option_Some hoist31 ->
+        | Core.Option.Option_Some hoist36 ->
           (match y <: Core.Option.t_Option u8 with
-            | Core.Option.Option_Some hoist30 ->
+            | Core.Option.Option_Some hoist35 ->
               (match
-                  Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist31 hoist30)
+                  Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist36 hoist35)
                   <:
                   Core.Option.t_Option u8
                 with
-                | Core.Option.Option_Some hoist34 ->
-                  (match hoist34 <: u8 with
+                | Core.Option.Option_Some hoist39 ->
+                  (match hoist39 <: u8 with
                     | 3uy ->
                       (match Core.Option.Option_None <: Core.Option.t_Option u8 with
                         | Core.Option.Option_Some some ->
                           let v:u8 = some in
                           (match x <: Core.Option.t_Option u8 with
-                            | Core.Option.Option_Some hoist35 ->
+                            | Core.Option.Option_Some hoist40 ->
                               (match y <: Core.Option.t_Option u8 with
-                                | Core.Option.Option_Some hoist36 ->
+                                | Core.Option.Option_Some hoist41 ->
                                   Core.Option.Option_Some
                                   (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
-                                          hoist35
+                                          hoist40
                                         <:
                                         u8)
-                                      hoist36)
+                                      hoist41)
                                   <:
                                   Core.Option.t_Option u8
                                 | Core.Option.Option_None  ->
@@ -392,18 +417,18 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
                           Core.Option.Option_None <: Core.Option.t_Option u8)
                     | 4uy ->
                       (match z <: Core.Option.t_Option u64 with
-                        | Core.Option.Option_Some hoist23 ->
-                          let v:u8 = 4uy +! (if hoist23 >. 4uL <: bool then 0uy else 3uy) in
+                        | Core.Option.Option_Some hoist28 ->
+                          let v:u8 = 4uy +! (if hoist28 >. 4uL <: bool then 0uy else 3uy) in
                           (match x <: Core.Option.t_Option u8 with
-                            | Core.Option.Option_Some hoist35 ->
+                            | Core.Option.Option_Some hoist40 ->
                               (match y <: Core.Option.t_Option u8 with
-                                | Core.Option.Option_Some hoist36 ->
+                                | Core.Option.Option_Some hoist41 ->
                                   Core.Option.Option_Some
                                   (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
-                                          hoist35
+                                          hoist40
                                         <:
                                         u8)
-                                      hoist36)
+                                      hoist41)
                                   <:
                                   Core.Option.t_Option u8
                                 | Core.Option.Option_None  ->
@@ -415,15 +440,15 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
                     | _ ->
                       let v:u8 = 12uy in
                       match x <: Core.Option.t_Option u8 with
-                      | Core.Option.Option_Some hoist35 ->
+                      | Core.Option.Option_Some hoist40 ->
                         (match y <: Core.Option.t_Option u8 with
-                          | Core.Option.Option_Some hoist36 ->
+                          | Core.Option.Option_Some hoist41 ->
                             Core.Option.Option_Some
                             (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
-                                    hoist35
+                                    hoist40
                                   <:
                                   u8)
-                                hoist36)
+                                hoist41)
                             <:
                             Core.Option.t_Option u8
                           | Core.Option.Option_None  ->
@@ -463,8 +488,8 @@ let simplifiable_question_mark (c: bool) (x: Core.Option.t_Option i32) : Core.Op
   if c
   then
     match x <: Core.Option.t_Option i32 with
-    | Core.Option.Option_Some hoist40 ->
-      let a:i32 = hoist40 +! 10l in
+    | Core.Option.Option_Some hoist45 ->
+      let a:i32 = hoist45 +! 10l in
       let b:i32 = 20l in
       Core.Option.Option_Some (a +! b) <: Core.Option.t_Option i32
     | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option i32
diff --git a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap
index 2f2304adb..a3aebbf34 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap	
+++ b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap	
@@ -130,6 +130,8 @@ Notation "'Build_t_Foo' '[' x ']' '(' 'f_bar' ':=' y ')'" := (Build_t_Foo (f_x :
 
 (*Not implemented yet? todo(item)*)
 
+(*Not implemented yet? todo(item)*)
+
 Equations add3 {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 int32) (y : both L2 I2 int32) (z : both L3 I3 int32) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32 :=
   add3 x y z  :=
     solve_lift (impl__u32__wrapping_add (impl__u32__wrapping_add x y) z) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32.
@@ -153,31 +155,31 @@ Fail Next Obligation.
 
 Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) :=
   direct_result_question_mark_coercion y  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist5 := impl__map_err y f_from in
-    Result_Ok (Result_Ok hoist5))) : both L1 I1 (t_Result int8 int32).
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist12 := impl__map_err y f_from in
+    Result_Ok (Result_Ok hoist12))) : both L1 I1 (t_Result int8 int32).
 Fail Next Obligation.
 
 Equations early_returns {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 int32 :=
   early_returns x  :=
     solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (3 : int32))
-    then letm[choice_typeMonad.result_bind_code int32] hoist6 := ControlFlow_Break (ret_both (0 : int32)) in
-    ControlFlow_Continue (never_to_any hoist6)
+    then letm[choice_typeMonad.result_bind_code int32] hoist13 := ControlFlow_Break (ret_both (0 : int32)) in
+    ControlFlow_Continue (never_to_any hoist13)
     else () in
-    letb hoist7 := x >.? (ret_both (30 : int32)) in
-    letm[choice_typeMonad.result_bind_code int32] hoist9 := ifb hoist7
+    letb hoist14 := x >.? (ret_both (30 : int32)) in
+    letm[choice_typeMonad.result_bind_code int32] hoist16 := ifb hoist14
     then matchb ret_both (true : 'bool) with
     | true =>
-      letm[choice_typeMonad.result_bind_code int32] hoist8 := ControlFlow_Break (ret_both (34 : int32)) in
-      ControlFlow_Continue (solve_lift (never_to_any hoist8))
+      letm[choice_typeMonad.result_bind_code int32] hoist15 := ControlFlow_Break (ret_both (34 : int32)) in
+      ControlFlow_Continue (solve_lift (never_to_any hoist15))
     | _ =>
       ControlFlow_Continue (solve_lift (ret_both (3 : int32)))
     end
     else ControlFlow_Continue (letb _ := assign todo(term) in
     x .+ (ret_both (1 : int32))) in
-    letb hoist10 := impl__u32__wrapping_add (ret_both (123 : int32)) hoist9 in
-    letb hoist11 := impl__u32__wrapping_add hoist10 x in
-    letm[choice_typeMonad.result_bind_code int32] hoist12 := ControlFlow_Break hoist11 in
-    ControlFlow_Continue (never_to_any hoist12))) : both L1 I1 int32.
+    letb hoist17 := impl__u32__wrapping_add (ret_both (123 : int32)) hoist16 in
+    letb hoist18 := impl__u32__wrapping_add hoist17 x in
+    letm[choice_typeMonad.result_bind_code int32] hoist19 := ControlFlow_Break hoist18 in
+    ControlFlow_Continue (never_to_any hoist19))) : both L1 I1 int32.
 Fail Next Obligation.
 
 Definition y_loc : Location :=
@@ -188,27 +190,27 @@ Equations local_mutation {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1
   local_mutation x  :=
     letb y loc(y_loc) := ret_both (0 : int32) in
     letb _ := assign todo(term) in
-    letb hoist13 := x >.? (ret_both (3 : int32)) in
-    solve_lift (ifb hoist13
+    letb hoist20 := x >.? (ret_both (3 : int32)) in
+    solve_lift (ifb hoist20
     then letb _ := assign todo(term) in
     letb y loc(y_loc) := x ./ (ret_both (2 : int32)) in
     letb _ := assign todo(term) in
-    letb hoist14 := ret_both (0 : int32) in
-    letb hoist15 := Build_t_Range (f_start := hoist14) (f_end := ret_both (10 : int32)) in
-    letb hoist16 := f_into_iter hoist15 in
-    letb _ := foldi_both_list hoist16 (fun i =>
+    letb hoist21 := ret_both (0 : int32) in
+    letb hoist22 := Build_t_Range (f_start := hoist21) (f_end := ret_both (10 : int32)) in
+    letb hoist23 := f_into_iter hoist22 in
+    letb _ := foldi_both_list hoist23 (fun i =>
       ssp (fun _ =>
         assign todo(term) : (both (*0*)(L1:|:fset []) (I1) 'unit))) (ret_both (tt : 'unit)) in
     impl__u32__wrapping_add x y
-    else letb hoist19 := matchb x with
+    else letb hoist26 := matchb x with
     | 12 =>
       letb _ := assign todo(term) in
       solve_lift (ret_both (3 : int32))
     | 13 =>
-      letb hoist18 := x in
+      letb hoist25 := x in
       letb _ := assign todo(term) in
-      letb hoist17 := impl__u32__wrapping_add (ret_both (123 : int32)) x in
-      solve_lift (add3 hoist18 hoist17 x)
+      letb hoist24 := impl__u32__wrapping_add (ret_both (123 : int32)) x in
+      solve_lift (add3 hoist25 hoist24 x)
     | _ =>
       solve_lift (ret_both (0 : int32))
     end in
@@ -219,44 +221,44 @@ Fail Next Obligation.
 Equations monad_lifting {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result t_A t_B) :=
   monad_lifting x  :=
     solve_lift (run (ifb x >.? (ret_both (123 : int8))
-    then letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist20 := ControlFlow_Continue (Result_Err B) in
-    letb hoist21 := Result_Ok hoist20 in
-    letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist22 := ControlFlow_Break hoist21 in
-    ControlFlow_Continue (never_to_any hoist22)
+    then letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist27 := ControlFlow_Continue (Result_Err B) in
+    letb hoist28 := Result_Ok hoist27 in
+    letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist29 := ControlFlow_Break hoist28 in
+    ControlFlow_Continue (never_to_any hoist29)
     else ControlFlow_Continue (Result_Ok A))) : both L1 I1 (t_Result t_A t_B).
 Fail Next Obligation.
 
 Equations options {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 (t_Option int8)) (y : both L2 I2 (t_Option int8)) (z : both L3 I3 (t_Option int64)) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8) :=
   options x y z  :=
-    solve_lift (run (letm[choice_typeMonad.option_bind_code] hoist26 := x in
-    letb hoist27 := hoist26 >.? (ret_both (10 : int8)) in
-    letm[choice_typeMonad.option_bind_code] hoist33 := ifb hoist27
-    then letm[choice_typeMonad.option_bind_code] hoist28 := x in
-    Option_Some (letb hoist29 := impl__u8__wrapping_add hoist28 (ret_both (3 : int8)) in
-    Option_Some hoist29)
-    else letm[choice_typeMonad.option_bind_code] hoist31 := x in
-    letm[choice_typeMonad.option_bind_code] hoist30 := y in
-    Option_Some (letb hoist32 := impl__u8__wrapping_add hoist31 hoist30 in
-    Option_Some hoist32) in
-    letm[choice_typeMonad.option_bind_code] hoist34 := hoist33 in
-    letm[choice_typeMonad.option_bind_code] v := matchb hoist34 with
+    solve_lift (run (letm[choice_typeMonad.option_bind_code] hoist33 := x in
+    letb hoist34 := hoist33 >.? (ret_both (10 : int8)) in
+    letm[choice_typeMonad.option_bind_code] hoist40 := ifb hoist34
+    then letm[choice_typeMonad.option_bind_code] hoist35 := x in
+    Option_Some (letb hoist36 := impl__u8__wrapping_add hoist35 (ret_both (3 : int8)) in
+    Option_Some hoist36)
+    else letm[choice_typeMonad.option_bind_code] hoist38 := x in
+    letm[choice_typeMonad.option_bind_code] hoist37 := y in
+    Option_Some (letb hoist39 := impl__u8__wrapping_add hoist38 hoist37 in
+    Option_Some hoist39) in
+    letm[choice_typeMonad.option_bind_code] hoist41 := hoist40 in
+    letm[choice_typeMonad.option_bind_code] v := matchb hoist41 with
     | 3 =>
       Option_None
     | 4 =>
-      letm[choice_typeMonad.option_bind_code] hoist23 := z in
-      Option_Some (letb hoist24 := hoist23 >.? (ret_both (4 : int64)) in
-      letb hoist25 := ifb hoist24
+      letm[choice_typeMonad.option_bind_code] hoist30 := z in
+      Option_Some (letb hoist31 := hoist30 >.? (ret_both (4 : int64)) in
+      letb hoist32 := ifb hoist31
       then ret_both (0 : int8)
       else ret_both (3 : int8) in
-      solve_lift ((ret_both (4 : int8)) .+ hoist25))
+      solve_lift ((ret_both (4 : int8)) .+ hoist32))
     | _ =>
       Option_Some (solve_lift (ret_both (12 : int8)))
     end in
-    letm[choice_typeMonad.option_bind_code] hoist35 := x in
-    letb hoist37 := impl__u8__wrapping_add v hoist35 in
-    letm[choice_typeMonad.option_bind_code] hoist36 := y in
-    Option_Some (letb hoist38 := impl__u8__wrapping_add hoist37 hoist36 in
-    Option_Some hoist38))) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8).
+    letm[choice_typeMonad.option_bind_code] hoist42 := x in
+    letb hoist44 := impl__u8__wrapping_add v hoist42 in
+    letm[choice_typeMonad.option_bind_code] hoist43 := y in
+    Option_Some (letb hoist45 := impl__u8__wrapping_add hoist44 hoist43 in
+    Option_Some hoist45))) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8).
 Fail Next Obligation.
 
 Definition y_loc : Location :=
@@ -268,8 +270,8 @@ Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
     letb _ := assign todo(term) in
-    letb hoist39 := x >.? (ret_both (90 : int32)) in
-    ifb hoist39
+    letb hoist46 := x >.? (ret_both (90 : int32)) in
+    ifb hoist46
     then impl__map_err (Result_Err (ret_both (12 : int8))) f_from
     else ()
     else () in
@@ -279,8 +281,8 @@ Fail Next Obligation.
 Equations simplifiable_question_mark {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (c : both L1 I1 'bool) (x : both L2 I2 (t_Option int32)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32) :=
   simplifiable_question_mark c x  :=
     solve_lift (run (letm[choice_typeMonad.option_bind_code] a := ifb c
-    then letm[choice_typeMonad.option_bind_code] hoist40 := x in
-    Option_Some (hoist40 .+ (ret_both (10 : int32)))
+    then letm[choice_typeMonad.option_bind_code] hoist47 := x in
+    Option_Some (hoist47 .+ (ret_both (10 : int32)))
     else Option_Some (ret_both (0 : int32)) in
     Option_Some (letb b := ret_both (20 : int32) in
     Option_Some (a .+ b)))) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32).
@@ -295,8 +297,8 @@ Equations simplifiable_return {L1 : {fset Location}} {L2 : {fset Location}} {L3
     then letm[choice_typeMonad.result_bind_code int32] _ := ifb c2
     then letb _ := assign todo(term) in
     ifb c3
-    then letm[choice_typeMonad.result_bind_code int32] hoist41 := ControlFlow_Break (ret_both (1 : int32)) in
-    ControlFlow_Continue (never_to_any hoist41)
+    then letm[choice_typeMonad.result_bind_code int32] hoist48 := ControlFlow_Break (ret_both (1 : int32)) in
+    ControlFlow_Continue (never_to_any hoist48)
     else ()
     else () in
     ControlFlow_Continue (letb _ := assign todo(term) in
@@ -388,3 +390,58 @@ Equations test {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I
     hoist4)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32).
 Fail Next Obligation.
 '''
+"Side_effects_Nested_return.v" = '''
+(* File automatically generated by Hacspec *)
+Set Warnings "-notation-overridden,-ambiguous-paths".
+From Crypt Require Import choice_type Package Prelude.
+Import PackageNotation.
+From extructures Require Import ord fset.
+From mathcomp Require Import word_ssrZ word.
+From Jasmin Require Import word.
+
+From Coq Require Import ZArith.
+From Coq Require Import Strings.String.
+Import List.ListNotations.
+Open Scope list_scope.
+Open Scope Z_scope.
+Open Scope bool_scope.
+
+From Hacspec Require Import ChoiceEquality.
+From Hacspec Require Import LocationUtility.
+From Hacspec Require Import Hacspec_Lib_Comparable.
+From Hacspec Require Import Hacspec_Lib_Pre.
+From Hacspec Require Import Hacspec_Lib.
+
+Open Scope hacspec_scope.
+Import choice.Choice.Exports.
+
+Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
+
+Equations other_fun {L1 : {fset Location}} {I1 : Interface} (rng : both L1 I1 int8) : both L1 I1 (int8 × t_Result 'unit 'unit) :=
+  other_fun rng  :=
+    letb hax_temp_output := Result_Ok (ret_both (tt : 'unit)) in
+    solve_lift (prod_b (rng,hax_temp_output)) : both L1 I1 (int8 × t_Result 'unit 'unit).
+Fail Next Obligation.
+
+Equations fun {L1 : {fset Location}} {I1 : Interface} (rng : both L1 I1 int8) : both L1 I1 (int8 × t_Result 'unit 'unit) :=
+  fun rng  :=
+    solve_lift (run (letb '(tmp0,out) := other_fun rng in
+    letb _ := assign todo(term) in
+    letb hoist6 := out in
+    letb hoist7 := f_branch hoist6 in
+    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist8 := matchb hoist7 with
+    | ControlFlow_Break_case residual =>
+      letb residual := ret_both ((residual) : (t_Result t_Infallible 'unit)) in
+      letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist5 := ControlFlow_Break (prod_b (rng,f_from_residual residual)) in
+      ControlFlow_Continue (solve_lift (never_to_any hoist5))
+    | ControlFlow_Continue_case val =>
+      letb val := ret_both ((val) : ('unit)) in
+      ControlFlow_Continue (solve_lift val)
+    end in
+    letb hoist9 := Result_Ok hoist8 in
+    letb hoist10 := prod_b (rng,hoist9) in
+    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist11 := ControlFlow_Break hoist10 in
+    ControlFlow_Continue (letb hax_temp_output := never_to_any hoist11 in
+    prod_b (rng,hax_temp_output)))) : both L1 I1 (int8 × t_Result 'unit 'unit).
+Fail Next Obligation.
+'''
diff --git a/tests/side-effects/src/lib.rs b/tests/side-effects/src/lib.rs
index 6c8f45a19..feb2eba44 100644
--- a/tests/side-effects/src/lib.rs
+++ b/tests/side-effects/src/lib.rs
@@ -179,3 +179,14 @@ mod issue_1089 {
         x.map(|i| Some(i + y?))?
     }
 }
+
+/// issue 1175
+mod nested_return {
+    fn other_fun(rng: &mut i8) -> Result<(), ()> {
+        Ok(())
+    }
+
+    fn fun(rng: &mut i8) -> Result<(), ()> {
+        return Ok(other_fun(rng)?);
+    }
+}