Repository: cryspen/hax (language: rust)

Issue:
Question mark in a closure gives an error
```rust

fn test(x: Option<i32>, y: Option<i32>) -> Option<i32> {
    x.map(|i| Some(i + y?))?
}

```
[Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/31458e07fe/gist=1a3da6e8ad09c6d1e0eebaab0f87c65c)

This gives the following error:

```
error: [HAX0002] (DropReturnBreakContinue) Fatal error: something we considered as impossible occurred! Please report this by submitting an issue on GitHub!
Details: Return/Break/Continue are expected to be gone as this point
 --> src/lib.rs:3:24
  |
3 |     x.map(|i| Some(i + y?))?
```

This is another regression from #393.


Discussion / hints:

Fix patch:
diff --git a/engine/lib/phases/phase_drop_return_break_continue.ml b/engine/lib/phases/phase_drop_return_break_continue.ml
index 3be7e8b1f..937bfeb69 100644
--- a/engine/lib/phases/phase_drop_return_break_continue.ml
+++ b/engine/lib/phases/phase_drop_return_break_continue.ml
@@ -118,6 +118,18 @@ module%inlined_contents Make (F : Features.T) = struct
                  in exit nodes. **)
       end
 
+    let closure_visitor =
+      let module Visitors = Ast_visitors.Make (F) in
+      object
+        inherit [_] Visitors.map as super
+
+        method! visit_expr' () e =
+          match e with
+          | Closure ({ body; _ } as closure) ->
+              Closure { closure with body = visitor#visit_expr None body }
+          | _ -> super#visit_expr' () e
+      end
+
     [%%inline_defs dmutability + dsafety_kind]
 
     let rec dexpr' (span : span) (expr : A.expr') : B.expr' =
@@ -157,7 +169,8 @@ module%inlined_contents Make (F : Features.T) = struct
     [%%inline_defs "Item.*" - ditems]
 
     let ditems (items : A.item list) : B.item list =
-      List.concat_map items ~f:(visitor#visit_item None >> ditem)
+      List.concat_map items
+        ~f:(visitor#visit_item None >> closure_visitor#visit_item () >> ditem)
   end
 
   include Implem


Test patch:
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 e03cc7117..a2038278d 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
@@ -58,6 +58,27 @@ let f (x: u8) : Core.Result.t_Result u16 u16 =
     <:
     Core.Result.t_Result u16 u16
 '''
+"Side_effects.Issue_1089_.fst" = '''
+module Side_effects.Issue_1089_
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let test (x y: Core.Option.t_Option i32) : Core.Option.t_Option i32 =
+  match
+    Core.Option.impl__map #i32
+      #(Core.Option.t_Option i32)
+      x
+      (fun i ->
+          let i:i32 = i in
+          match y with
+          | Core.Option.Option_Some hoist1 ->
+            Core.Option.Option_Some (i +! hoist1 <: i32) <: Core.Option.t_Option i32
+          | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option i32)
+  with
+  | Core.Option.Option_Some some -> some
+  | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option i32
+'''
 "Side_effects.fst" = '''
 module Side_effects
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -185,7 +206,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 with
-  | Core.Result.Result_Ok hoist1 -> Core.Result.Result_Ok hoist1 <: Core.Result.t_Result i8 u32
+  | Core.Result.Result_Ok hoist5 -> Core.Result.Result_Ok hoist5 <: 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)
     <:
@@ -201,12 +222,12 @@ let early_returns (x: u32) : u32 =
       match true with
       | true -> 34ul
       | _ ->
-        let x, hoist5:(u32 & u32) = x, 3ul <: (u32 & u32) in
-        Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist5 <: u32) x
+        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
     else
       let x:u32 = x +! 9ul in
-      let x, hoist5:(u32 & u32) = x, x +! 1ul <: (u32 & u32) in
-      Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist5 <: u32) x
+      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
 
 /// Exercise local mutation with control flow and loops
 let local_mutation (x: u32) : u32 =
@@ -234,7 +255,7 @@ let local_mutation (x: u32) : u32 =
     in
     Core.Num.impl__u32__wrapping_add x y
   else
-    let (x, y), hoist15:((u32 & u32) & u32) =
+    let (x, y), hoist19:((u32 & u32) & u32) =
       match x with
       | 12ul ->
         let y:u32 = Core.Num.impl__u32__wrapping_add x y in
@@ -246,7 +267,7 @@ let local_mutation (x: u32) : u32 =
         ((u32 & u32) & u32)
       | _ -> (x, y <: (u32 & u32)), 0ul <: ((u32 & u32) & u32)
     in
-    let x:u32 = hoist15 in
+    let x:u32 = hoist19 in
     Core.Num.impl__u32__wrapping_add x y
 
 /// Combine `?` and early return
@@ -254,39 +275,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 hoist16 -> Core.Result.Result_Ok hoist16 <: Core.Result.t_Result t_A t_B
+    | Core.Result.Result_Ok hoist20 -> Core.Result.Result_Ok hoist20 <: 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 with
-  | Core.Option.Option_Some hoist22 ->
-    if hoist22 >. 10uy
+  | Core.Option.Option_Some hoist26 ->
+    if hoist26 >. 10uy
     then
       match x with
-      | Core.Option.Option_Some hoist24 ->
+      | Core.Option.Option_Some hoist28 ->
         (match
-            Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist24 3uy)
+            Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist28 3uy)
             <:
             Core.Option.t_Option u8
           with
-          | Core.Option.Option_Some hoist30 ->
-            (match hoist30 with
+          | Core.Option.Option_Some hoist34 ->
+            (match hoist34 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 with
-                      | Core.Option.Option_Some hoist31 ->
+                      | Core.Option.Option_Some hoist35 ->
                         (match y with
-                          | Core.Option.Option_Some hoist32 ->
+                          | Core.Option.Option_Some hoist36 ->
                             Core.Option.Option_Some
                             (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
-                                    hoist31
+                                    hoist35
                                   <:
                                   u8)
-                                hoist32)
+                                hoist36)
                             <:
                             Core.Option.t_Option u8
                           | Core.Option.Option_None  ->
@@ -296,18 +317,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 with
-                  | Core.Option.Option_Some hoist19 ->
-                    let v:u8 = 4uy +! (if hoist19 >. 4uL <: bool then 0uy else 3uy) in
+                  | Core.Option.Option_Some hoist23 ->
+                    let v:u8 = 4uy +! (if hoist23 >. 4uL <: bool then 0uy else 3uy) in
                     (match x with
-                      | Core.Option.Option_Some hoist31 ->
+                      | Core.Option.Option_Some hoist35 ->
                         (match y with
-                          | Core.Option.Option_Some hoist32 ->
+                          | Core.Option.Option_Some hoist36 ->
                             Core.Option.Option_Some
                             (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
-                                    hoist31
+                                    hoist35
                                   <:
                                   u8)
-                                hoist32)
+                                hoist36)
                             <:
                             Core.Option.t_Option u8
                           | Core.Option.Option_None  ->
@@ -318,14 +339,14 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
               | _ ->
                 let v:u8 = 12uy in
                 match x with
-                | Core.Option.Option_Some hoist31 ->
+                | Core.Option.Option_Some hoist35 ->
                   (match y with
-                    | Core.Option.Option_Some hoist32 ->
+                    | Core.Option.Option_Some hoist36 ->
                       Core.Option.Option_Some
-                      (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v hoist31
+                      (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v hoist35
                             <:
                             u8)
-                          hoist32)
+                          hoist36)
                       <:
                       Core.Option.t_Option u8
                     | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option u8
@@ -335,30 +356,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 with
-        | Core.Option.Option_Some hoist27 ->
+        | Core.Option.Option_Some hoist31 ->
           (match y with
-            | Core.Option.Option_Some hoist26 ->
+            | Core.Option.Option_Some hoist30 ->
               (match
-                  Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist27 hoist26)
+                  Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist31 hoist30)
                   <:
                   Core.Option.t_Option u8
                 with
-                | Core.Option.Option_Some hoist30 ->
-                  (match hoist30 with
+                | Core.Option.Option_Some hoist34 ->
+                  (match hoist34 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 with
-                            | Core.Option.Option_Some hoist31 ->
+                            | Core.Option.Option_Some hoist35 ->
                               (match y with
-                                | Core.Option.Option_Some hoist32 ->
+                                | Core.Option.Option_Some hoist36 ->
                                   Core.Option.Option_Some
                                   (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
-                                          hoist31
+                                          hoist35
                                         <:
                                         u8)
-                                      hoist32)
+                                      hoist36)
                                   <:
                                   Core.Option.t_Option u8
                                 | Core.Option.Option_None  ->
@@ -369,18 +390,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 with
-                        | Core.Option.Option_Some hoist19 ->
-                          let v:u8 = 4uy +! (if hoist19 >. 4uL <: bool then 0uy else 3uy) in
+                        | Core.Option.Option_Some hoist23 ->
+                          let v:u8 = 4uy +! (if hoist23 >. 4uL <: bool then 0uy else 3uy) in
                           (match x with
-                            | Core.Option.Option_Some hoist31 ->
+                            | Core.Option.Option_Some hoist35 ->
                               (match y with
-                                | Core.Option.Option_Some hoist32 ->
+                                | Core.Option.Option_Some hoist36 ->
                                   Core.Option.Option_Some
                                   (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
-                                          hoist31
+                                          hoist35
                                         <:
                                         u8)
-                                      hoist32)
+                                      hoist36)
                                   <:
                                   Core.Option.t_Option u8
                                 | Core.Option.Option_None  ->
@@ -392,15 +413,15 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
                     | _ ->
                       let v:u8 = 12uy in
                       match x with
-                      | Core.Option.Option_Some hoist31 ->
+                      | Core.Option.Option_Some hoist35 ->
                         (match y with
-                          | Core.Option.Option_Some hoist32 ->
+                          | Core.Option.Option_Some hoist36 ->
                             Core.Option.Option_Some
                             (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
-                                    hoist31
+                                    hoist35
                                   <:
                                   u8)
-                                hoist32)
+                                hoist36)
                             <:
                             Core.Option.t_Option u8
                           | Core.Option.Option_None  ->
@@ -440,8 +461,8 @@ let simplifiable_question_mark (c: bool) (x: Core.Option.t_Option i32) : Core.Op
   if c
   then
     match x with
-    | Core.Option.Option_Some hoist36 ->
-      let a:i32 = hoist36 +! 10l in
+    | Core.Option.Option_Some hoist40 ->
+      let a:i32 = hoist40 +! 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 80a576172..2f2304adb 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap
+++ b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap
@@ -128,6 +128,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.
@@ -151,31 +153,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] hoist1 := impl__map_err y f_from in
-    Result_Ok (Result_Ok hoist1))) : both L1 I1 (t_Result int8 int32).
+    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).
 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] hoist2 := ControlFlow_Break (ret_both (0 : int32)) in
-    ControlFlow_Continue (never_to_any hoist2)
+    then letm[choice_typeMonad.result_bind_code int32] hoist6 := ControlFlow_Break (ret_both (0 : int32)) in
+    ControlFlow_Continue (never_to_any hoist6)
     else () in
-    letb hoist3 := x >.? (ret_both (30 : int32)) in
-    letm[choice_typeMonad.result_bind_code int32] hoist5 := ifb hoist3
+    letb hoist7 := x >.? (ret_both (30 : int32)) in
+    letm[choice_typeMonad.result_bind_code int32] hoist9 := ifb hoist7
     then matchb ret_both (true : 'bool) with
     | true =>
-      letm[choice_typeMonad.result_bind_code int32] hoist4 := ControlFlow_Break (ret_both (34 : int32)) in
-      ControlFlow_Continue (solve_lift (never_to_any hoist4))
+      letm[choice_typeMonad.result_bind_code int32] hoist8 := ControlFlow_Break (ret_both (34 : int32)) in
+      ControlFlow_Continue (solve_lift (never_to_any hoist8))
     | _ =>
       ControlFlow_Continue (solve_lift (ret_both (3 : int32)))
     end
     else ControlFlow_Continue (letb _ := assign todo(term) in
     x .+ (ret_both (1 : int32))) in
-    letb hoist6 := impl__u32__wrapping_add (ret_both (123 : int32)) hoist5 in
-    letb hoist7 := impl__u32__wrapping_add hoist6 x in
-    letm[choice_typeMonad.result_bind_code int32] hoist8 := ControlFlow_Break hoist7 in
-    ControlFlow_Continue (never_to_any hoist8))) : both L1 I1 int32.
+    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.
 Fail Next Obligation.
 
 Definition y_loc : Location :=
@@ -186,27 +188,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 hoist9 := x >.? (ret_both (3 : int32)) in
-    solve_lift (ifb hoist9
+    letb hoist13 := x >.? (ret_both (3 : int32)) in
+    solve_lift (ifb hoist13
     then letb _ := assign todo(term) in
     letb y loc(y_loc) := x ./ (ret_both (2 : int32)) in
     letb _ := assign todo(term) in
-    letb hoist10 := ret_both (0 : int32) in
-    letb hoist11 := Build_t_Range (f_start := hoist10) (f_end := ret_both (10 : int32)) in
-    letb hoist12 := f_into_iter hoist11 in
-    letb _ := foldi_both_list hoist12 (fun i =>
+    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 =>
       ssp (fun _ =>
         assign todo(term) : (both (*0*)(L1:|:fset []) (I1) 'unit))) (ret_both (tt : 'unit)) in
     impl__u32__wrapping_add x y
-    else letb hoist15 := matchb x with
+    else letb hoist19 := matchb x with
     | 12 =>
       letb _ := assign todo(term) in
       solve_lift (ret_both (3 : int32))
     | 13 =>
-      letb hoist14 := x in
+      letb hoist18 := x in
       letb _ := assign todo(term) in
-      letb hoist13 := impl__u32__wrapping_add (ret_both (123 : int32)) x in
-      solve_lift (add3 hoist14 hoist13 x)
+      letb hoist17 := impl__u32__wrapping_add (ret_both (123 : int32)) x in
+      solve_lift (add3 hoist18 hoist17 x)
     | _ =>
       solve_lift (ret_both (0 : int32))
     end in
@@ -217,44 +219,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)] hoist16 := ControlFlow_Continue (Result_Err B) in
-    letb hoist17 := Result_Ok hoist16 in
-    letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist18 := ControlFlow_Break hoist17 in
-    ControlFlow_Continue (never_to_any hoist18)
+    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)
     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] hoist22 := x in
-    letb hoist23 := hoist22 >.? (ret_both (10 : int8)) in
-    letm[choice_typeMonad.option_bind_code] hoist29 := ifb hoist23
-    then letm[choice_typeMonad.option_bind_code] hoist24 := x in
-    Option_Some (letb hoist25 := impl__u8__wrapping_add hoist24 (ret_both (3 : int8)) in
-    Option_Some hoist25)
-    else letm[choice_typeMonad.option_bind_code] hoist27 := x in
-    letm[choice_typeMonad.option_bind_code] hoist26 := y in
-    Option_Some (letb hoist28 := impl__u8__wrapping_add hoist27 hoist26 in
-    Option_Some hoist28) in
-    letm[choice_typeMonad.option_bind_code] hoist30 := hoist29 in
-    letm[choice_typeMonad.option_bind_code] v := matchb hoist30 with
+    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
     | 3 =>
       Option_None
     | 4 =>
-      letm[choice_typeMonad.option_bind_code] hoist19 := z in
-      Option_Some (letb hoist20 := hoist19 >.? (ret_both (4 : int64)) in
-      letb hoist21 := ifb hoist20
+      letm[choice_typeMonad.option_bind_code] hoist23 := z in
+      Option_Some (letb hoist24 := hoist23 >.? (ret_both (4 : int64)) in
+      letb hoist25 := ifb hoist24
       then ret_both (0 : int8)
       else ret_both (3 : int8) in
-      solve_lift ((ret_both (4 : int8)) .+ hoist21))
+      solve_lift ((ret_both (4 : int8)) .+ hoist25))
     | _ =>
       Option_Some (solve_lift (ret_both (12 : int8)))
     end in
-    letm[choice_typeMonad.option_bind_code] hoist31 := x in
-    letb hoist33 := impl__u8__wrapping_add v hoist31 in
-    letm[choice_typeMonad.option_bind_code] hoist32 := y in
-    Option_Some (letb hoist34 := impl__u8__wrapping_add hoist33 hoist32 in
-    Option_Some hoist34))) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8).
+    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).
 Fail Next Obligation.
 
 Definition y_loc : Location :=
@@ -266,8 +268,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 hoist35 := x >.? (ret_both (90 : int32)) in
-    ifb hoist35
+    letb hoist39 := x >.? (ret_both (90 : int32)) in
+    ifb hoist39
     then impl__map_err (Result_Err (ret_both (12 : int8))) f_from
     else ()
     else () in
@@ -277,8 +279,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] hoist36 := x in
-    Option_Some (hoist36 .+ (ret_both (10 : int32)))
+    then letm[choice_typeMonad.option_bind_code] hoist40 := x in
+    Option_Some (hoist40 .+ (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).
@@ -293,8 +295,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] hoist37 := ControlFlow_Break (ret_both (1 : int32)) in
-    ControlFlow_Continue (never_to_any hoist37)
+    then letm[choice_typeMonad.result_bind_code int32] hoist41 := ControlFlow_Break (ret_both (1 : int32)) in
+    ControlFlow_Continue (never_to_any hoist41)
     else ()
     else () in
     ControlFlow_Continue (letb _ := assign todo(term) in
@@ -349,3 +351,40 @@ Equations f {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both
     Result_Ok (Result_Ok (f_my_from x)))) : both L1 I1 (t_Result int16 int16).
 Fail Next Obligation.
 '''
+"Side_effects_Issue_1089_.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 test {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (x : both L1 I1 (t_Option int32)) (y : both L2 I2 (t_Option int32)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32) :=
+  test x y  :=
+    solve_lift (run (letb hoist3 := fun i =>
+      letm[choice_typeMonad.option_bind_code] hoist1 := y in
+      Option_Some (letb hoist2 := i .+ hoist1 in
+      Option_Some hoist2) in
+    letb hoist4 := impl__map x hoist3 in
+    hoist4)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32).
+Fail Next Obligation.
+'''
diff --git a/tests/side-effects/src/lib.rs b/tests/side-effects/src/lib.rs
index c7db53f22..6c8f45a19 100644
--- a/tests/side-effects/src/lib.rs
+++ b/tests/side-effects/src/lib.rs
@@ -173,3 +173,9 @@ mod issue_1083 {
         Ok(u16::my_from(x))
     }
 }
+
+mod issue_1089 {
+    fn test(x: Option<i32>, y: Option<i32>) -> Option<i32> {
+        x.map(|i| Some(i + y?))?
+    }
+}