Merge pull request #227 from AeneasVerif/son/clean-synthesis

Remove the use of `Option` from the functions synthesizing the symbolic AST

14 files changed, 339 insertions, 417 deletions

diff --git a/compiler/Cps.ml b/compiler/Cps.ml
index f7694ba2..917989ff 100644
--- a/compiler/Cps.ml
+++ b/compiler/Cps.ml
@@ -35,23 +35,24 @@ type statement_eval_res =
        *)
 [@@deriving show]
 
-type eval_result = SymbolicAst.expression option
-
 (** Function which takes a context as input, and evaluates to:
     - a new context
     - a continuation with which to build the execution trace, provided the
       trace for the end of the execution.
   *)
-type cm_fun = eval_ctx -> eval_ctx * (eval_result -> eval_result)
+type cm_fun =
+  eval_ctx -> eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
 
 type st_cm_fun =
-  eval_ctx -> (eval_ctx * statement_eval_res) * (eval_result -> eval_result)
+  eval_ctx ->
+  (eval_ctx * statement_eval_res)
+  * (SymbolicAst.expression -> SymbolicAst.expression)
 
 (** Type of a function used when evaluating a statement *)
 type stl_cm_fun =
   eval_ctx ->
   (eval_ctx * statement_eval_res) list
-  * (SymbolicAst.expression list option -> eval_result)
+  * (SymbolicAst.expression list -> SymbolicAst.expression)
 
 (** Compose continuations that we use to compute execution traces *)
 let cc_comp (f : 'b -> 'c) (g : 'a -> 'b) : 'a -> 'c = fun e -> f (g e)
@@ -90,27 +91,11 @@ let map_apply_continuation (f : 'a -> 'c -> 'b * 'c * ('e -> 'e))
   in
   eval_list inputs ctx
 
-let opt_list_to_list_opt (len : int) (el : 'a option list) : 'a list option =
-  let expr_list =
-    List.rev
-      (List.fold_left
-         (fun acc a -> match a with Some b -> b :: acc | None -> [])
-         [] el)
-  in
-  let _ = assert (List.length expr_list = len) in
-  if Option.is_none (List.hd expr_list) then None else Some expr_list
-
 let cc_singleton file line span cf el =
-  match el with
-  | Some [ e ] -> cf (Some e)
-  | Some _ -> internal_error file line span
-  | _ -> None
+  match el with [ e ] -> cf e | _ -> internal_error file line span
 
 let cf_singleton file line span el =
-  match el with
-  | Some [ e ] -> Some e
-  | Some _ -> internal_error file line span
-  | _ -> None
+  match el with [ e ] -> e | _ -> internal_error file line span
 
 (** It happens that we need to concatenate lists of results, for
     instance when evaluating the branches of a match. When applying
@@ -120,15 +105,11 @@ let cf_singleton file line span el =
  *)
 let comp_seqs (file : string) (line : int) (span : Meta.span)
     (ls :
-      ('a list
-      * (SymbolicAst.expression list option -> SymbolicAst.expression option))
-      list) :
-    'a list
-    * (SymbolicAst.expression list option -> SymbolicAst.expression list option)
-    =
+      ('a list * (SymbolicAst.expression list -> SymbolicAst.expression)) list)
+    : 'a list * (SymbolicAst.expression list -> SymbolicAst.expression list) =
   (* Auxiliary function: given a list of expressions el, build the expressions
      corresponding to the different branches *)
-  let rec cc_aux ls el =
+  let rec cc ls el =
     match ls with
     | [] ->
         (* End of the list of branches: there shouldn't be any expression remaining *)
@@ -140,14 +121,10 @@ let comp_seqs (file : string) (line : int) (span : Meta.span)
            - the expressions for the remaining branches *)
         let el0, el = Collections.List.split_at el (List.length resl) in
         (* Compute the expression for the current branch *)
-        let e0 = cf (Some el0) in
-        let e0 =
-          match e0 with None -> internal_error file line span | Some e -> e
-        in
+        let e0 = cf el0 in
         (* Compute the expressions for the remaining branches *)
-        let e = cc_aux ls el in
+        let e = cc ls el in
         (* Concatenate *)
         e0 :: e
   in
-  let cc el = match el with None -> None | Some el -> Some (cc_aux ls el) in
-  (List.flatten (fst (List.split ls)), cc)
+  (List.flatten (fst (List.split ls)), cc ls)
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 94158979..fb3701f3 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -277,7 +277,7 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
 let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
     (fdef : fun_decl) (inst_sg : inst_fun_sig) (back_id : RegionGroupId.id)
     (loop_id : LoopId.id option) (is_regular_return : bool) (inside_loop : bool)
-    (ctx : eval_ctx) : SA.expression option =
+    (ctx : eval_ctx) : SA.expression =
   log#ldebug
     (lazy
       ("evaluate_function_symbolic_synthesize_backward_from_return:"
@@ -477,8 +477,8 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
   (* Generate the Return node *)
   let return_expr =
     match loop_id with
-    | None -> Some (SA.Return (ctx, None))
-    | Some loop_id -> Some (SA.ReturnWithLoop (loop_id, inside_loop))
+    | None -> SA.Return (ctx, None)
+    | Some loop_id -> SA.ReturnWithLoop (loop_id, inside_loop)
   in
   (* Apply *)
   cc return_expr
@@ -486,12 +486,12 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
 (** Evaluate a function with the symbolic interpreter.
 
     We return:
-    - the list of symbolic values introduced for the input values (this is useful
-      for the synthesis)
+    - the list of symbolic values introduced for the input values (this is
+      useful for the synthesis)
     - the symbolic AST generated by the symbolic execution
  *)
-let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
-    (fdef : fun_decl) : symbolic_value list * SA.expression option =
+let evaluate_function_symbolic (ctx : decls_ctx) (fdef : fun_decl) :
+    symbolic_value list * SA.expression =
   (* Debug *)
   let name_to_string () =
     Print.Types.name_to_string
@@ -518,101 +518,92 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
 
     match res with
     | Return | LoopReturn _ ->
-        if synthesize then
-          (* We have to "play different endings":
-           * - one execution for the forward function
-           * - one execution per backward function
-           * We then group everything together.
-           *)
-          (* There are two cases:
-           * - if this is a forward translation, we retrieve the returned value.
-           * - if this is a backward translation, we introduce "return"
-           *   abstractions to consume the return value, then end all the
-           *   abstractions up to the one in which we are interested.
-           *)
-          (* Forward translation: retrieve the returned value *)
-          let fwd_e =
-            (* Pop the frame and retrieve the returned value at the same time *)
-            let pop_return_value = true in
-            let ret_value, ctx, cc_pop =
-              pop_frame config fdef.item_meta.span pop_return_value ctx
-            in
-            (* Generate the Return node *)
-            cc_pop (Some (SA.Return (ctx, ret_value)))
-          in
-          let fwd_e = Option.get fwd_e in
-          (* Backward translation: introduce "return"
-             abstractions to consume the return value, then end all the
-             abstractions up to the one in which we are interested.
-          *)
-          let loop_id =
-            match res with
-            | Return -> None
-            | LoopReturn loop_id -> Some loop_id
-            | _ -> craise __FILE__ __LINE__ fdef.item_meta.span "Unreachable"
-          in
-          let is_regular_return = true in
-          let inside_loop = Option.is_some loop_id in
-          let finish_back_eval back_id =
-            Option.get
-              (evaluate_function_symbolic_synthesize_backward_from_return config
-                 fdef inst_sg back_id loop_id is_regular_return inside_loop ctx)
-          in
-          let back_el =
-            RegionGroupId.mapi
-              (fun gid _ -> (gid, finish_back_eval gid))
-              regions_hierarchy
+        (* We have to "play different endings":
+         * - one execution for the forward function
+         * - one execution per backward function
+         * We then group everything together.
+         *)
+        (* There are two cases:
+         * - if this is a forward translation, we retrieve the returned value.
+         * - if this is a backward translation, we introduce "return"
+         *   abstractions to consume the return value, then end all the
+         *   abstractions up to the one in which we are interested.
+         *)
+        (* Forward translation: retrieve the returned value *)
+        let fwd_e =
+          (* Pop the frame and retrieve the returned value at the same time *)
+          let pop_return_value = true in
+          let ret_value, ctx, cc_pop =
+            pop_frame config fdef.item_meta.span pop_return_value ctx
           in
-          let back_el = RegionGroupId.Map.of_list back_el in
-          (* Put everything together *)
-          synthesize_forward_end ctx0 None fwd_e back_el
-        else None
+          (* Generate the Return node *)
+          cc_pop (SA.Return (ctx, ret_value))
+        in
+        (* Backward translation: introduce "return"
+           abstractions to consume the return value, then end all the
+           abstractions up to the one in which we are interested.
+        *)
+        let loop_id =
+          match res with
+          | Return -> None
+          | LoopReturn loop_id -> Some loop_id
+          | _ -> craise __FILE__ __LINE__ fdef.item_meta.span "Unreachable"
+        in
+        let is_regular_return = true in
+        let inside_loop = Option.is_some loop_id in
+        let finish_back_eval back_id =
+          evaluate_function_symbolic_synthesize_backward_from_return config fdef
+            inst_sg back_id loop_id is_regular_return inside_loop ctx
+        in
+        let back_el =
+          RegionGroupId.mapi
+            (fun gid _ -> (gid, finish_back_eval gid))
+            regions_hierarchy
+        in
+        let back_el = RegionGroupId.Map.of_list back_el in
+        (* Put everything together *)
+        synthesize_forward_end ctx0 None fwd_e back_el
     | EndEnterLoop (loop_id, loop_input_values)
     | EndContinue (loop_id, loop_input_values) ->
         (* Similar to [Return]: we have to play different endings *)
-        if synthesize then
-          let inside_loop =
-            match res with
-            | EndEnterLoop _ -> false
-            | EndContinue _ -> true
-            | _ -> craise __FILE__ __LINE__ fdef.item_meta.span "Unreachable"
-          in
-          (* Forward translation *)
-          let fwd_e =
-            (* Pop the frame - there is no returned value to pop: in the
-               translation we will simply call the loop function *)
-            let pop_return_value = false in
-            let _ret_value, _ctx, cc_pop =
-              pop_frame config fdef.item_meta.span pop_return_value ctx
-            in
-            (* Generate the Return node *)
-            cc_pop (Some (SA.ReturnWithLoop (loop_id, inside_loop)))
-          in
-          let fwd_e = Option.get fwd_e in
-          (* Backward translation: introduce "return"
-             abstractions to consume the return value, then end all the
-             abstractions up to the one in which we are interested.
-          *)
-          let is_regular_return = false in
-          let finish_back_eval back_id =
-            Option.get
-              (evaluate_function_symbolic_synthesize_backward_from_return config
-                 fdef inst_sg back_id (Some loop_id) is_regular_return
-                 inside_loop ctx)
-          in
-          let back_el =
-            RegionGroupId.mapi
-              (fun gid _ -> (gid, finish_back_eval gid))
-              regions_hierarchy
+        let inside_loop =
+          match res with
+          | EndEnterLoop _ -> false
+          | EndContinue _ -> true
+          | _ -> craise __FILE__ __LINE__ fdef.item_meta.span "Unreachable"
+        in
+        (* Forward translation *)
+        let fwd_e =
+          (* Pop the frame - there is no returned value to pop: in the
+             translation we will simply call the loop function *)
+          let pop_return_value = false in
+          let _ret_value, _ctx, cc_pop =
+            pop_frame config fdef.item_meta.span pop_return_value ctx
           in
-          let back_el = RegionGroupId.Map.of_list back_el in
-          (* Put everything together *)
-          synthesize_forward_end ctx0 (Some loop_input_values) fwd_e back_el
-        else None
+          (* Generate the Return node *)
+          cc_pop (SA.ReturnWithLoop (loop_id, inside_loop))
+        in
+        (* Backward translation: introduce "return"
+           abstractions to consume the return value, then end all the
+           abstractions up to the one in which we are interested.
+        *)
+        let is_regular_return = false in
+        let finish_back_eval back_id =
+          evaluate_function_symbolic_synthesize_backward_from_return config fdef
+            inst_sg back_id (Some loop_id) is_regular_return inside_loop ctx
+        in
+        let back_el =
+          RegionGroupId.mapi
+            (fun gid _ -> (gid, finish_back_eval gid))
+            regions_hierarchy
+        in
+        let back_el = RegionGroupId.Map.of_list back_el in
+        (* Put everything together *)
+        synthesize_forward_end ctx0 (Some loop_input_values) fwd_e back_el
     | Panic ->
         (* Note that as we explore all the execution branches, one of
          * the executions can lead to a panic *)
-        if synthesize then Some SA.Panic else None
+        SA.Panic
     | Unit | Break _ | Continue _ ->
         craise __FILE__ __LINE__ fdef.item_meta.span
           ("evaluate_function_symbolic failed on: " ^ name_to_string ())
@@ -624,12 +615,9 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
       let ctx_resl, cc =
         eval_function_body config (Option.get fdef.body).body ctx
       in
-      let el =
-        List.map Option.get
-          (List.map (fun (ctx, res) -> finish res ctx) ctx_resl)
-      in
-      cc (Some el)
-    with CFailure (span, msg) -> Some (Error (span, msg))
+      let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in
+      cc el
+    with CFailure (span, msg) -> Error (span, msg)
   in
   (* Return *)
   (input_svs, symbolic)
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 4393e89f..41190618 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -446,9 +446,7 @@ let expand_symbolic_value_borrow (config : config) (span : Meta.span)
 let expand_symbolic_bool (config : config) (span : Meta.span)
     (sv : symbolic_value) (sv_place : SA.mplace option) :
     eval_ctx ->
-    (eval_ctx * eval_ctx)
-    * ((SymbolicAst.expression * SymbolicAst.expression) option -> eval_result)
-    =
+    (eval_ctx * eval_ctx) * (SA.expression * SA.expression -> SA.expression) =
  fun ctx ->
   (* Compute the expanded value *)
   let original_sv = sv in
@@ -465,9 +463,8 @@ let expand_symbolic_bool (config : config) (span : Meta.span)
   let ctx_true = apply_expansion see_true in
   let ctx_false = apply_expansion see_false in
   (* Compute the continuation to build the expression *)
-  let cf e =
-    let el = match e with Some (a, b) -> Some [ a; b ] | None -> None in
-    S.synthesize_symbolic_expansion span sv sv_place seel el
+  let cf (e0, e1) =
+    S.synthesize_symbolic_expansion span sv sv_place seel [ e0; e1 ]
   in
   (* Return *)
   ((ctx_true, ctx_false), cf)
@@ -535,8 +532,7 @@ let expand_symbolic_value_no_branching (config : config) (span : Meta.span)
 
 let expand_symbolic_adt (config : config) (span : Meta.span)
     (sv : symbolic_value) (sv_place : SA.mplace option) :
-    eval_ctx ->
-    eval_ctx list * (SymbolicAst.expression list option -> eval_result) =
+    eval_ctx -> eval_ctx list * (SA.expression list -> SA.expression) =
  fun ctx ->
   (* Debug *)
   log#ldebug (lazy ("expand_symbolic_adt:" ^ symbolic_value_to_string ctx sv));
@@ -571,8 +567,7 @@ let expand_symbolic_int (config : config) (span : Meta.span)
     (int_type : integer_type) (tgts : scalar_value list) :
     eval_ctx ->
     (eval_ctx list * eval_ctx)
-    * ((SymbolicAst.expression list * SymbolicAst.expression) option ->
-      eval_result) =
+    * (SA.expression list * SA.expression -> SA.expression) =
  fun ctx ->
   (* Sanity check *)
   sanity_check __FILE__ __LINE__ (sv.sv_ty = TLiteral (TInteger int_type)) span;
@@ -589,13 +584,10 @@ let expand_symbolic_int (config : config) (span : Meta.span)
   in
   let ctx_otherwise = ctx in
   (* Update the symbolic ast *)
-  let cf e =
-    match e with
-    | None -> None
-    | Some (el, e) ->
-        let seel = List.map (fun x -> Some x) seel in
-        S.synthesize_symbolic_expansion span sv sv_place (seel @ [ None ])
-          (Some (el @ [ e ]))
+  let cf (el, e) =
+    let seel = List.map (fun x -> Some x) seel in
+    S.synthesize_symbolic_expansion span sv sv_place (seel @ [ None ])
+      (el @ [ e ])
   in
   ((ctx_branches, ctx_otherwise), cf)
 
diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli
index 7f8c3a0a..50554490 100644
--- a/compiler/InterpreterExpansion.mli
+++ b/compiler/InterpreterExpansion.mli
@@ -38,7 +38,7 @@ val expand_symbolic_adt :
   symbolic_value ->
   SA.mplace option ->
   eval_ctx ->
-  eval_ctx list * (SymbolicAst.expression list option -> eval_result)
+  eval_ctx list * (SA.expression list -> SA.expression)
 
 (** Expand a symbolic boolean.
 
@@ -50,8 +50,7 @@ val expand_symbolic_bool :
   symbolic_value ->
   SA.mplace option ->
   eval_ctx ->
-  (eval_ctx * eval_ctx)
-  * ((SymbolicAst.expression * SymbolicAst.expression) option -> eval_result)
+  (eval_ctx * eval_ctx) * (SA.expression * SA.expression -> SA.expression)
 
 (** Symbolic integers are expanded upon evaluating a [SwitchInt].
 
@@ -76,8 +75,7 @@ val expand_symbolic_int :
   scalar_value list ->
   eval_ctx ->
   (eval_ctx list * eval_ctx)
-  * ((SymbolicAst.expression list * SymbolicAst.expression) option ->
-    eval_result)
+  * (SA.expression list * SA.expression -> SA.expression)
 
 (** If this mode is activated through the [config], greedily expand the symbolic
     values which need to be expanded. See {!type:Contexts.config} for more information.
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 56c0ab5f..5088d29a 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -67,7 +67,9 @@ let read_place_check (span : Meta.span) (access : access_kind) (p : place)
 
 let access_rplace_reorganize_and_read (config : config) (span : Meta.span)
     (expand_prim_copy : bool) (access : access_kind) (p : place)
-    (ctx : eval_ctx) : typed_value * eval_ctx * (eval_result -> eval_result) =
+    (ctx : eval_ctx) :
+    typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
+    =
   (* Make sure we can evaluate the path *)
   let ctx, cc = update_ctx_along_read_place config span access p ctx in
   (* End the proper loans at the place itself *)
@@ -264,7 +266,8 @@ let prepare_eval_operand_reorganize (config : config) (span : Meta.span)
 (** Evaluate an operand, without reorganizing the context before *)
 let eval_operand_no_reorganize (config : config) (span : Meta.span)
     (op : operand) (ctx : eval_ctx) :
-    typed_value * eval_ctx * (eval_result -> eval_result) =
+    typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
+    =
   (* Debug *)
   log#ldebug
     (lazy
@@ -287,16 +290,12 @@ let eval_operand_no_reorganize (config : config) (span : Meta.span)
           let v = mk_fresh_symbolic_typed_value span ty in
           (* Wrap the generated expression *)
           let cf e =
-            match e with
-            | None -> None
-            | Some e ->
-                Some
-                  (SymbolicAst.IntroSymbolic
-                     ( ctx0,
-                       None,
-                       value_as_symbolic span v.value,
-                       SymbolicAst.VaTraitConstValue (trait_ref, const_name),
-                       e ))
+            SymbolicAst.IntroSymbolic
+              ( ctx0,
+                None,
+                value_as_symbolic span v.value,
+                SymbolicAst.VaTraitConstValue (trait_ref, const_name),
+                e )
           in
           (v, ctx, cf)
       | CVar vid ->
@@ -321,20 +320,16 @@ let eval_operand_no_reorganize (config : config) (span : Meta.span)
           in
           (* We have to wrap the generated expression *)
           let cf e =
-            match e with
-            | None -> None
-            | Some e ->
-                (* If we are synthesizing a symbolic AST, it means that we are in symbolic
-                   mode: the value of the const generic is necessarily symbolic. *)
-                sanity_check __FILE__ __LINE__ (is_symbolic cv.value) span;
-                (* *)
-                Some
-                  (SymbolicAst.IntroSymbolic
-                     ( ctx0,
-                       None,
-                       value_as_symbolic span cv.value,
-                       SymbolicAst.VaCgValue vid,
-                       e ))
+            (* If we are synthesizing a symbolic AST, it means that we are in symbolic
+               mode: the value of the const generic is necessarily symbolic. *)
+            sanity_check __FILE__ __LINE__ (is_symbolic cv.value) span;
+            (* *)
+            SymbolicAst.IntroSymbolic
+              ( ctx0,
+                None,
+                value_as_symbolic span cv.value,
+                SymbolicAst.VaCgValue vid,
+                e )
           in
           (cv, ctx, cf)
       | CFnPtr _ ->
@@ -371,7 +366,9 @@ let eval_operand_no_reorganize (config : config) (span : Meta.span)
       (v, ctx, fun e -> e)
 
 let eval_operand (config : config) (span : Meta.span) (op : operand)
-    (ctx : eval_ctx) : typed_value * eval_ctx * (eval_result -> eval_result) =
+    (ctx : eval_ctx) :
+    typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
+    =
   (* Debug *)
   log#ldebug
     (lazy
@@ -393,7 +390,9 @@ let prepare_eval_operands_reorganize (config : config) (span : Meta.span)
 (** Evaluate several operands. *)
 let eval_operands (config : config) (span : Meta.span) (ops : operand list)
     (ctx : eval_ctx) :
-    typed_value list * eval_ctx * (eval_result -> eval_result) =
+    typed_value list
+    * eval_ctx
+    * (SymbolicAst.expression -> SymbolicAst.expression) =
   (* Prepare the operands *)
   let ctx, cc = prepare_eval_operands_reorganize config span ops ctx in
   (* Evaluate the operands *)
@@ -402,7 +401,9 @@ let eval_operands (config : config) (span : Meta.span) (ops : operand list)
 
 let eval_two_operands (config : config) (span : Meta.span) (op1 : operand)
     (op2 : operand) (ctx : eval_ctx) :
-    (typed_value * typed_value) * eval_ctx * (eval_result -> eval_result) =
+    (typed_value * typed_value)
+    * eval_ctx
+    * (SymbolicAst.expression -> SymbolicAst.expression) =
   let res, ctx, cc = eval_operands config span [ op1; op2 ] ctx in
   let res =
     match res with
@@ -413,7 +414,9 @@ let eval_two_operands (config : config) (span : Meta.span) (op1 : operand)
 
 let eval_unary_op_concrete (config : config) (span : Meta.span) (unop : unop)
     (op : operand) (ctx : eval_ctx) :
-    (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
+    (typed_value, eval_error) result
+    * eval_ctx
+    * (SymbolicAst.expression -> SymbolicAst.expression) =
   (* Evaluate the operand *)
   let v, ctx, cc = eval_operand config span op ctx in
   (* Apply the unop *)
@@ -463,7 +466,9 @@ let eval_unary_op_concrete (config : config) (span : Meta.span) (unop : unop)
 
 let eval_unary_op_symbolic (config : config) (span : Meta.span) (unop : unop)
     (op : operand) (ctx : eval_ctx) :
-    (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
+    (typed_value, eval_error) result
+    * eval_ctx
+    * (SymbolicAst.expression -> SymbolicAst.expression) =
   (* Evaluate the operand *)
   let v, ctx, cc = eval_operand config span op ctx in
   (* Generate a fresh symbolic value to store the result *)
@@ -489,7 +494,9 @@ let eval_unary_op_symbolic (config : config) (span : Meta.span) (unop : unop)
 
 let eval_unary_op (config : config) (span : Meta.span) (unop : unop)
     (op : operand) (ctx : eval_ctx) :
-    (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
+    (typed_value, eval_error) result
+    * eval_ctx
+    * (SymbolicAst.expression -> SymbolicAst.expression) =
   match config.mode with
   | ConcreteMode -> eval_unary_op_concrete config span unop op ctx
   | SymbolicMode -> eval_unary_op_symbolic config span unop op ctx
@@ -573,7 +580,9 @@ let eval_binary_op_concrete_compute (span : Meta.span) (binop : binop)
 
 let eval_binary_op_concrete (config : config) (span : Meta.span) (binop : binop)
     (op1 : operand) (op2 : operand) (ctx : eval_ctx) :
-    (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
+    (typed_value, eval_error) result
+    * eval_ctx
+    * (SymbolicAst.expression -> SymbolicAst.expression) =
   (* Evaluate the operands *)
   let (v1, v2), ctx, cc = eval_two_operands config span op1 op2 ctx in
   (* Compute the result of the binop *)
@@ -583,7 +592,9 @@ let eval_binary_op_concrete (config : config) (span : Meta.span) (binop : binop)
 
 let eval_binary_op_symbolic (config : config) (span : Meta.span) (binop : binop)
     (op1 : operand) (op2 : operand) (ctx : eval_ctx) :
-    (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
+    (typed_value, eval_error) result
+    * eval_ctx
+    * (SymbolicAst.expression -> SymbolicAst.expression) =
   (* Evaluate the operands *)
   let (v1, v2), ctx, cc = eval_two_operands config span op1 op2 ctx in
   (* Generate a fresh symbolic value to store the result *)
@@ -631,7 +642,9 @@ let eval_binary_op_symbolic (config : config) (span : Meta.span) (binop : binop)
 
 let eval_binary_op (config : config) (span : Meta.span) (binop : binop)
     (op1 : operand) (op2 : operand) (ctx : eval_ctx) :
-    (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
+    (typed_value, eval_error) result
+    * eval_ctx
+    * (SymbolicAst.expression -> SymbolicAst.expression) =
   match config.mode with
   | ConcreteMode -> eval_binary_op_concrete config span binop op1 op2 ctx
   | SymbolicMode -> eval_binary_op_symbolic config span binop op1 op2 ctx
@@ -640,7 +653,8 @@ let eval_binary_op (config : config) (span : Meta.span) (binop : binop)
     `&p` or `&mut p` or `&two-phase p`) *)
 let eval_rvalue_ref (config : config) (span : Meta.span) (p : place)
     (bkind : borrow_kind) (ctx : eval_ctx) :
-    typed_value * eval_ctx * (eval_result -> eval_result) =
+    typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
+    =
   match bkind with
   | BShared | BTwoPhaseMut | BShallow ->
       (* **REMARK**: we initially treated shallow borrows like shared borrows.
@@ -723,7 +737,8 @@ let eval_rvalue_ref (config : config) (span : Meta.span) (p : place)
 
 let eval_rvalue_aggregate (config : config) (span : Meta.span)
     (aggregate_kind : aggregate_kind) (ops : operand list) (ctx : eval_ctx) :
-    typed_value * eval_ctx * (eval_result -> eval_result) =
+    typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
+    =
   (* Evaluate the operands *)
   let values, ctx, cc = eval_operands config span ops ctx in
   (* Compute the value *)
@@ -783,13 +798,9 @@ let eval_rvalue_aggregate (config : config) (span : Meta.span)
         let saggregated = mk_fresh_symbolic_typed_value span ty in
         (* Update the symbolic ast *)
         let cf e =
-          match e with
-          | None -> None
-          | Some e ->
-              (* Introduce the symbolic value in the AST *)
-              let sv = ValuesUtils.value_as_symbolic span saggregated.value in
-              Some
-                (SymbolicAst.IntroSymbolic (ctx, None, sv, VaArray values, e))
+          (* Introduce the symbolic value in the AST *)
+          let sv = ValuesUtils.value_as_symbolic span saggregated.value in
+          SymbolicAst.IntroSymbolic (ctx, None, sv, VaArray values, e)
         in
         (saggregated, cf)
     | AggregatedClosure _ ->
@@ -799,7 +810,9 @@ let eval_rvalue_aggregate (config : config) (span : Meta.span)
 
 let eval_rvalue_not_global (config : config) (span : Meta.span)
     (rvalue : rvalue) (ctx : eval_ctx) :
-    (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) =
+    (typed_value, eval_error) result
+    * eval_ctx
+    * (SymbolicAst.expression -> SymbolicAst.expression) =
   log#ldebug (lazy "eval_rvalue");
   (* Small helper *)
   let wrap_in_result (v, ctx, cc) = (Ok v, ctx, cc) in
diff --git a/compiler/InterpreterExpressions.mli b/compiler/InterpreterExpressions.mli
index feb641d1..29234ea9 100644
--- a/compiler/InterpreterExpressions.mli
+++ b/compiler/InterpreterExpressions.mli
@@ -25,7 +25,7 @@ val access_rplace_reorganize_and_read :
   access_kind ->
   place ->
   eval_ctx ->
-  typed_value * eval_ctx * (eval_result -> eval_result)
+  typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
 
 (** Evaluate an operand.
 
@@ -41,7 +41,7 @@ val eval_operand :
   Meta.span ->
   operand ->
   eval_ctx ->
-  typed_value * eval_ctx * (eval_result -> eval_result)
+  typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
 
 (** Evaluate several operands at once. *)
 val eval_operands :
@@ -49,7 +49,9 @@ val eval_operands :
   Meta.span ->
   operand list ->
   eval_ctx ->
-  typed_value list * eval_ctx * (eval_result -> eval_result)
+  typed_value list
+  * eval_ctx
+  * (SymbolicAst.expression -> SymbolicAst.expression)
 
 (** Evaluate an rvalue which is not a global (globals are handled elsewhere).
 
@@ -63,7 +65,9 @@ val eval_rvalue_not_global :
   Meta.span ->
   rvalue ->
   eval_ctx ->
-  (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result)
+  (typed_value, eval_error) result
+  * eval_ctx
+  * (SymbolicAst.expression -> SymbolicAst.expression)
 
 (** Evaluate a fake read (update the context so that we can read a place) *)
 val eval_fake_read : config -> Meta.span -> place -> cm_fun
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 90161196..c33c34a6 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -64,10 +64,7 @@ let eval_loop_concrete (span : Meta.span) (eval_loop_body : stl_cm_fun) :
      the loop body at least once *)
   let ctx_resl = rec_eval_loop_body ctx (Continue 0) in
   (* If we evaluate in concrete mode, we shouldn't have to generate any symbolic expression *)
-  let cf el =
-    sanity_check __FILE__ __LINE__ (el = None) span;
-    None
-  in
+  let cf _ = internal_error __FILE__ __LINE__ span in
   (ctx_resl, cf)
 
 (** Auxiliary function for {!eval_loop_symbolic}.
@@ -92,7 +89,8 @@ let eval_loop_symbolic_synthesize_fun_end (config : config) (span : span)
     (loop_id : LoopId.id) (init_ctx : eval_ctx) (fixed_ids : ids_sets)
     (fp_ctx : eval_ctx) (fp_input_svalues : SymbolicValueId.id list)
     (rg_to_abs : AbstractionId.id RegionGroupId.Map.t) :
-    ((eval_ctx * statement_eval_res) * (eval_result -> eval_result))
+    ((eval_ctx * statement_eval_res)
+    * (SymbolicAst.expression -> SymbolicAst.expression))
     * borrow_loan_corresp =
   (* First, preemptively end borrows/move values by matching the current
      context with the target context *)
@@ -212,7 +210,7 @@ let eval_loop_symbolic_synthesize_loop_body (config : config) (span : span)
     (fp_ctx : eval_ctx) (fp_input_svalues : SymbolicValueId.id list)
     (fp_bl_corresp : borrow_loan_corresp) :
     (eval_ctx * statement_eval_res) list
-    * (SymbolicAst.expression list option -> eval_result) =
+    * (SymbolicAst.expression list -> SymbolicAst.expression) =
   (* First, evaluate the loop body starting from the **fixed-point** context *)
   let ctx_resl, cf_loop = eval_loop_body fp_ctx in
 
@@ -252,16 +250,9 @@ let eval_loop_symbolic_synthesize_loop_body (config : config) (span : span)
 
   (* Apply and compose *)
   let ctx_resl, cfl = List.split (List.map eval_after_loop_iter ctx_resl) in
-  let cc (el : SymbolicAst.expression list option) : eval_result =
-    match el with
-    | None -> None
-    | Some el ->
-        let el =
-          List.map
-            (fun (cf, e) -> Option.get (cf (Some e)))
-            (List.combine cfl el)
-        in
-        cf_loop (Some el)
+  let cc (el : SymbolicAst.expression list) : SymbolicAst.expression =
+    let el = List.map (fun (cf, e) -> cf e) (List.combine cfl el) in
+    cf_loop el
   in
 
   (ctx_resl, cc)
@@ -380,17 +371,14 @@ let eval_loop_symbolic (config : config) (span : span)
   in
 
   (* Put everything together *)
-  let cc (el : SymbolicAst.expression list option) =
+  let cc (el : SymbolicAst.expression list) =
     match el with
-    | None -> None
-    | Some el -> (
-        match el with
-        | [] -> internal_error __FILE__ __LINE__ span
-        | e :: el ->
-            let fun_end_expr = cf_fun_end (Some e) in
-            let loop_expr = cf_loop_body (Some el) in
-            S.synthesize_loop loop_id input_svalues fresh_sids rg_to_given_back
-              fun_end_expr loop_expr span)
+    | [] -> internal_error __FILE__ __LINE__ span
+    | e :: el ->
+        let fun_end_expr = cf_fun_end e in
+        let loop_expr = cf_loop_body el in
+        S.synthesize_loop loop_id input_svalues fresh_sids rg_to_given_back
+          fun_end_expr loop_expr span
   in
   (res_fun_end :: resl_loop_body, cc)
 
diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index b68f2a4d..735f3743 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -371,19 +371,13 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) :
 
   (* Synthesize *)
   let cf e =
-    match e with
-    | None -> None
-    | Some e ->
-        (* Add the let-bindings which introduce the fresh symbolic values *)
-        Some
-          (List.fold_left
-             (fun e (sid, v) ->
-               let v = mk_typed_value_from_symbolic_value v in
-               let sv =
-                 SymbolicValueId.Map.find sid new_ctx_ids_map.sids_to_values
-               in
-               SymbolicAst.IntroSymbolic (ctx, None, sv, VaSingleValue v, e))
-             e !sid_subst)
+    (* Add the let-bindings which introduce the fresh symbolic values *)
+    List.fold_left
+      (fun e (sid, v) ->
+        let v = mk_typed_value_from_symbolic_value v in
+        let sv = SymbolicValueId.Map.find sid new_ctx_ids_map.sids_to_values in
+        SymbolicAst.IntroSymbolic (ctx, None, sv, VaSingleValue v, e))
+      e !sid_subst
   in
   (ctx, cf)
 
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index b2de3b22..8a924a0a 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -525,7 +525,8 @@ let rec update_ctx_along_write_place (config : config) (span : Meta.span)
       comp cc (update_ctx_along_write_place config span access p ctx)
 
 (** Small utility used to break control-flow *)
-exception UpdateCtx of (eval_ctx * (eval_result -> eval_result))
+exception
+  UpdateCtx of (eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression))
 
 let rec end_loans_at_place (config : config) (span : Meta.span)
     (access : access_kind) (p : place) : cm_fun =
@@ -631,7 +632,9 @@ let drop_outer_loans_at_lplace (config : config) (span : Meta.span) (p : place)
   (ctx, cc)
 
 let prepare_lplace (config : config) (span : Meta.span) (p : place)
-    (ctx : eval_ctx) : typed_value * eval_ctx * (eval_result -> eval_result) =
+    (ctx : eval_ctx) :
+    typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
+    =
   log#ldebug
     (lazy
       ("prepare_lplace:" ^ "\n- p: " ^ place_to_string ctx p
diff --git a/compiler/InterpreterPaths.mli b/compiler/InterpreterPaths.mli
index 86f0dcc0..3377f612 100644
--- a/compiler/InterpreterPaths.mli
+++ b/compiler/InterpreterPaths.mli
@@ -104,4 +104,4 @@ val prepare_lplace :
   Meta.span ->
   place ->
   eval_ctx ->
-  typed_value * eval_ctx * (eval_result -> eval_result)
+  typed_value * eval_ctx * (SymbolicAst.expression -> SymbolicAst.expression)
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 283a711d..27f503bc 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -306,7 +306,9 @@ let get_assumed_function_return_type (span : Meta.span) (ctx : eval_ctx)
 
 let move_return_value (config : config) (span : Meta.span)
     (pop_return_value : bool) (ctx : eval_ctx) :
-    typed_value option * eval_ctx * (eval_result -> eval_result) =
+    typed_value option
+    * eval_ctx
+    * (SymbolicAst.expression -> SymbolicAst.expression) =
   if pop_return_value then
     let ret_vid = VarId.zero in
     let v, ctx, cc =
@@ -317,7 +319,9 @@ let move_return_value (config : config) (span : Meta.span)
 
 let pop_frame (config : config) (span : Meta.span) (pop_return_value : bool)
     (ctx : eval_ctx) :
-    typed_value option * eval_ctx * (eval_result -> eval_result) =
+    typed_value option
+    * eval_ctx
+    * (SymbolicAst.expression -> SymbolicAst.expression) =
   (* Debug *)
   log#ldebug (lazy ("pop_frame:\n" ^ eval_ctx_to_string ~span:(Some span) ctx));
 
@@ -1033,7 +1037,7 @@ and eval_global (config : config) (span : Meta.span) (dest : place)
       let func = { func = FunId (FRegular global.body); generics } in
       let call = { func = FnOpRegular func; args = []; dest } in
       eval_transparent_function_call_concrete config span global.body call ctx
-  | SymbolicMode -> (
+  | SymbolicMode ->
       (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
        * defined as equal to the value of the global (see {!S.synthesize_global_eval}). *)
       cassert __FILE__ __LINE__ (ty_no_regions global.ty) span
@@ -1056,12 +1060,8 @@ and eval_global (config : config) (span : Meta.span) (dest : place)
           dest ctx
       in
       ( [ (ctx, Unit) ],
-        fun el ->
-          match el with
-          | Some [ e ] ->
-              (cc_comp (S.synthesize_global_eval gid generics sval) cc) (Some e)
-          | Some _ -> internal_error __FILE__ __LINE__ span
-          | _ -> None ))
+        cc_singleton __FILE__ __LINE__ span
+          (cc_comp (S.synthesize_global_eval gid generics sval) cc) )
 
 (** Evaluate a switch *)
 and eval_switch (config : config) (span : Meta.span) (switch : switch) :
@@ -1102,8 +1102,7 @@ and eval_switch (config : config) (span : Meta.span) (switch : switch) :
             in
             let cc el =
               match cf_branches el with
-              | None -> None
-              | Some [ e_true; e_false ] -> cf_bool (Some (e_true, e_false))
+              | [ e_true; e_false ] -> cf_bool (e_true, e_false)
               | _ -> internal_error __FILE__ __LINE__ span
             in
             (ctx_resl, cc)
@@ -1158,11 +1157,8 @@ and eval_switch (config : config) (span : Meta.span) (switch : switch) :
                 (resl_branches @ [ resl_otherwise ])
             in
             let cc el =
-              match el with
-              | None -> None
-              | Some el ->
-                  let el, e_otherwise = Collections.List.pop_last el in
-                  cf_int (Some (el, e_otherwise))
+              let el, e_otherwise = Collections.List.pop_last el in
+              cf_int (el, e_otherwise)
             in
             (resl, cc_comp cc cf)
         | _ -> craise __FILE__ __LINE__ span "Inconsistent state"
@@ -1235,7 +1231,7 @@ and eval_function_call_concrete (config : config) (span : Meta.span)
       match func.func with
       | FunId (FRegular fid) ->
           eval_transparent_function_call_concrete config span fid call ctx
-      | FunId (FAssumed fid) -> (
+      | FunId (FAssumed fid) ->
           (* Continue - note that we do as if the function call has been successful,
            * by giving {!Unit} to the continuation, because we place us in the case
            * where we haven't panicked. Of course, the translation needs to take the
@@ -1243,12 +1239,7 @@ and eval_function_call_concrete (config : config) (span : Meta.span)
           let ctx, cc =
             eval_assumed_function_call_concrete config span fid call ctx
           in
-          ( [ (ctx, Unit) ],
-            fun el ->
-              match el with
-              | Some [ e ] -> cc (Some e)
-              | Some _ -> internal_error __FILE__ __LINE__ span
-              | _ -> None ))
+          ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ span cc)
       | TraitMethod _ -> craise __FILE__ __LINE__ span "Unimplemented")
 
 and eval_function_call_symbolic (config : config) (span : Meta.span)
@@ -1351,13 +1342,7 @@ and eval_transparent_function_call_concrete (config : config) (span : Meta.span)
           ctx_resl
       in
       let ctx_resl, cfl = List.split ctx_resl_cfl in
-      let cf_pop el =
-        match el with
-        | None -> None
-        | Some el ->
-            Some
-              (List.map Option.get (List.map2 (fun cf e -> cf (Some e)) cfl el))
-      in
+      let cf_pop el = List.map2 (fun cf e -> cf e) cfl el in
       (* Continue *)
       (ctx_resl, cc_comp cc cf_pop)
 
@@ -1620,11 +1605,6 @@ and eval_function_body (config : config) (body : statement) : stl_cm_fun =
       ctx_resl
   in
   let ctx_resl, cfl = List.split ctx_res_cfl in
-  let cf_end el =
-    match el with
-    | None -> None
-    | Some el ->
-        Some (List.map Option.get (List.map2 (fun cf e -> cf (Some e)) cfl el))
-  in
+  let cf_end el = List.map2 (fun cf e -> cf e) cfl el in
   (* Compose and continue *)
   (ctx_resl, cc_comp cf_body cf_end)
diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli
index c70396d6..443f559e 100644
--- a/compiler/InterpreterStatements.mli
+++ b/compiler/InterpreterStatements.mli
@@ -21,7 +21,9 @@ val pop_frame :
   Meta.span ->
   bool ->
   eval_ctx ->
-  typed_value option * eval_ctx * (eval_result -> eval_result)
+  typed_value option
+  * eval_ctx
+  * (SymbolicAst.expression -> SymbolicAst.expression)
 
 (** Helper.
 
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index ae701c33..b15ab38a 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -25,110 +25,101 @@ let mk_espan (m : espan) (e : expression) : expression = Meta (m, e)
 
 let synthesize_symbolic_expansion (span : Meta.span) (sv : symbolic_value)
     (place : mplace option) (seel : symbolic_expansion option list)
-    (el : expression list option) : expression option =
-  match el with
-  | None -> None
-  | Some el ->
-      let ls = List.combine seel el in
-      (* Match on the symbolic value type to know which can of expansion happened *)
-      let expansion =
-        match sv.sv_ty with
-        | TLiteral TBool -> (
-            (* Boolean expansion: there should be two branches *)
-            match ls with
-            | [
-             (Some (SeLiteral (VBool true)), true_exp);
-             (Some (SeLiteral (VBool false)), false_exp);
-            ] ->
-                ExpandBool (true_exp, false_exp)
-            | _ -> craise __FILE__ __LINE__ span "Ill-formed boolean expansion")
-        | TLiteral (TInteger int_ty) ->
-            (* Switch over an integer: split between the "regular" branches
-               and the "otherwise" branch (which should be the last branch) *)
-            let branches, otherwise = Collections.List.pop_last ls in
-            (* For all the regular branches, the symbolic value should have
-             * been expanded to a constant *)
-            let get_scalar (see : symbolic_expansion option) : scalar_value =
-              match see with
-              | Some (SeLiteral (VScalar cv)) ->
-                  sanity_check __FILE__ __LINE__ (cv.int_ty = int_ty) span;
-                  cv
-              | _ -> craise __FILE__ __LINE__ span "Unreachable"
-            in
-            let branches =
-              List.map (fun (see, exp) -> (get_scalar see, exp)) branches
-            in
-            (* For the otherwise branch, the symbolic value should have been left
-             * unchanged *)
-            let otherwise_see, otherwise = otherwise in
-            sanity_check __FILE__ __LINE__ (otherwise_see = None) span;
-            (* Return *)
-            ExpandInt (int_ty, branches, otherwise)
-        | TAdt (_, _) ->
-            (* Branching: it is necessarily an enumeration expansion *)
-            let get_variant (see : symbolic_expansion option) :
-                VariantId.id option * symbolic_value list =
-              match see with
-              | Some (SeAdt (vid, fields)) -> (vid, fields)
-              | _ ->
-                  craise __FILE__ __LINE__ span
-                    "Ill-formed branching ADT expansion"
-            in
-            let exp =
-              List.map
-                (fun (see, exp) ->
-                  let vid, fields = get_variant see in
-                  (vid, fields, exp))
-                ls
-            in
-            ExpandAdt exp
-        | TRef (_, _, _) -> (
-            (* Reference expansion: there should be one branch *)
-            match ls with
-            | [ (Some see, exp) ] -> ExpandNoBranch (see, exp)
-            | _ -> craise __FILE__ __LINE__ span "Ill-formed borrow expansion")
-        | TVar _ | TLiteral TChar | TNever | TTraitType _ | TArrow _ | TRawPtr _
-          ->
-            craise __FILE__ __LINE__ span "Ill-formed symbolic expansion"
-      in
-      Some (Expansion (place, sv, expansion))
+    (el : expression list) : expression =
+  let ls = List.combine seel el in
+  (* Match on the symbolic value type to know which can of expansion happened *)
+  let expansion =
+    match sv.sv_ty with
+    | TLiteral TBool -> (
+        (* Boolean expansion: there should be two branches *)
+        match ls with
+        | [
+         (Some (SeLiteral (VBool true)), true_exp);
+         (Some (SeLiteral (VBool false)), false_exp);
+        ] ->
+            ExpandBool (true_exp, false_exp)
+        | _ -> craise __FILE__ __LINE__ span "Ill-formed boolean expansion")
+    | TLiteral (TInteger int_ty) ->
+        (* Switch over an integer: split between the "regular" branches
+           and the "otherwise" branch (which should be the last branch) *)
+        let branches, otherwise = Collections.List.pop_last ls in
+        (* For all the regular branches, the symbolic value should have
+         * been expanded to a constant *)
+        let get_scalar (see : symbolic_expansion option) : scalar_value =
+          match see with
+          | Some (SeLiteral (VScalar cv)) ->
+              sanity_check __FILE__ __LINE__ (cv.int_ty = int_ty) span;
+              cv
+          | _ -> craise __FILE__ __LINE__ span "Unreachable"
+        in
+        let branches =
+          List.map (fun (see, exp) -> (get_scalar see, exp)) branches
+        in
+        (* For the otherwise branch, the symbolic value should have been left
+         * unchanged *)
+        let otherwise_see, otherwise = otherwise in
+        sanity_check __FILE__ __LINE__ (otherwise_see = None) span;
+        (* Return *)
+        ExpandInt (int_ty, branches, otherwise)
+    | TAdt (_, _) ->
+        (* Branching: it is necessarily an enumeration expansion *)
+        let get_variant (see : symbolic_expansion option) :
+            VariantId.id option * symbolic_value list =
+          match see with
+          | Some (SeAdt (vid, fields)) -> (vid, fields)
+          | _ ->
+              craise __FILE__ __LINE__ span "Ill-formed branching ADT expansion"
+        in
+        let exp =
+          List.map
+            (fun (see, exp) ->
+              let vid, fields = get_variant see in
+              (vid, fields, exp))
+            ls
+        in
+        ExpandAdt exp
+    | TRef (_, _, _) -> (
+        (* Reference expansion: there should be one branch *)
+        match ls with
+        | [ (Some see, exp) ] -> ExpandNoBranch (see, exp)
+        | _ -> craise __FILE__ __LINE__ span "Ill-formed borrow expansion")
+    | TVar _ | TLiteral TChar | TNever | TTraitType _ | TArrow _ | TRawPtr _ ->
+        craise __FILE__ __LINE__ span "Ill-formed symbolic expansion"
+  in
+  Expansion (place, sv, expansion)
 
 let synthesize_symbolic_expansion_no_branching (span : Meta.span)
     (sv : symbolic_value) (place : mplace option) (see : symbolic_expansion)
-    (e : expression option) : expression option =
-  let el = Option.map (fun e -> [ e ]) e in
-  synthesize_symbolic_expansion span sv place [ Some see ] el
+    (e : expression) : expression =
+  synthesize_symbolic_expansion span sv place [ Some see ] [ e ]
 
 let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx)
     (sg : fun_sig option) (regions_hierarchy : region_var_groups)
     (abstractions : AbstractionId.id list) (generics : generic_args)
     (trait_method_generics : (generic_args * trait_instance_id) option)
     (args : typed_value list) (args_places : mplace option list)
-    (dest : symbolic_value) (dest_place : mplace option) (e : expression option)
-    : expression option =
-  Option.map
-    (fun e ->
-      let call =
-        {
-          call_id;
-          ctx;
-          sg;
-          regions_hierarchy;
-          abstractions;
-          generics;
-          trait_method_generics;
-          args;
-          dest;
-          args_places;
-          dest_place;
-        }
-      in
-      FunCall (call, e))
-    e
+    (dest : symbolic_value) (dest_place : mplace option) (e : expression) :
+    expression =
+  let call =
+    {
+      call_id;
+      ctx;
+      sg;
+      regions_hierarchy;
+      abstractions;
+      generics;
+      trait_method_generics;
+      args;
+      dest;
+      args_places;
+      dest_place;
+    }
+  in
+  FunCall (call, e)
 
 let synthesize_global_eval (gid : GlobalDeclId.id) (generics : generic_args)
-    (dest : symbolic_value) (e : expression option) : expression option =
-  Option.map (fun e -> EvalGlobal (gid, generics, dest, e)) e
+    (dest : symbolic_value) (e : expression) : expression =
+  EvalGlobal (gid, generics, dest, e)
 
 let synthesize_regular_function_call (fun_id : fun_id_or_trait_method_ref)
     (call_id : FunCallId.id) (ctx : Contexts.eval_ctx) (sg : fun_sig)
@@ -136,8 +127,8 @@ let synthesize_regular_function_call (fun_id : fun_id_or_trait_method_ref)
     (abstractions : AbstractionId.id list) (generics : generic_args)
     (trait_method_generics : (generic_args * trait_instance_id) option)
     (args : typed_value list) (args_places : mplace option list)
-    (dest : symbolic_value) (dest_place : mplace option) (e : expression option)
-    : expression option =
+    (dest : symbolic_value) (dest_place : mplace option) (e : expression) :
+    expression =
   synthesize_function_call
     (Fun (fun_id, call_id))
     ctx (Some sg) regions_hierarchy abstractions generics trait_method_generics
@@ -145,7 +136,7 @@ let synthesize_regular_function_call (fun_id : fun_id_or_trait_method_ref)
 
 let synthesize_unary_op (ctx : Contexts.eval_ctx) (unop : unop)
     (arg : typed_value) (arg_place : mplace option) (dest : symbolic_value)
-    (dest_place : mplace option) (e : expression option) : expression option =
+    (dest_place : mplace option) (e : expression) : expression =
   let generics = empty_generic_args in
   synthesize_function_call (Unop unop) ctx None [] [] generics None [ arg ]
     [ arg_place ] dest dest_place e
@@ -153,50 +144,43 @@ let synthesize_unary_op (ctx : Contexts.eval_ctx) (unop : unop)
 let synthesize_binary_op (ctx : Contexts.eval_ctx) (binop : binop)
     (arg0 : typed_value) (arg0_place : mplace option) (arg1 : typed_value)
     (arg1_place : mplace option) (dest : symbolic_value)
-    (dest_place : mplace option) (e : expression option) : expression option =
+    (dest_place : mplace option) (e : expression) : expression =
   let generics = empty_generic_args in
   synthesize_function_call (Binop binop) ctx None [] [] generics None
     [ arg0; arg1 ] [ arg0_place; arg1_place ] dest dest_place e
 
 let synthesize_end_abstraction (ctx : Contexts.eval_ctx) (abs : abs)
-    (e : expression option) : expression option =
-  Option.map (fun e -> EndAbstraction (ctx, abs, e)) e
+    (e : expression) : expression =
+  EndAbstraction (ctx, abs, e)
 
 let synthesize_assignment (ctx : Contexts.eval_ctx) (lplace : mplace)
-    (rvalue : typed_value) (rplace : mplace option) (e : expression option) :
-    expression option =
-  Option.map (fun e -> Meta (Assignment (ctx, lplace, rvalue, rplace), e)) e
+    (rvalue : typed_value) (rplace : mplace option) (e : expression) :
+    expression =
+  Meta (Assignment (ctx, lplace, rvalue, rplace), e)
 
 let synthesize_assertion (ctx : Contexts.eval_ctx) (v : typed_value)
-    (e : expression option) =
-  Option.map (fun e -> Assertion (ctx, v, e)) e
+    (e : expression) =
+  Assertion (ctx, v, e)
 
 let synthesize_forward_end (ctx : Contexts.eval_ctx)
     (loop_input_values : typed_value SymbolicValueId.Map.t option)
     (e : expression) (el : expression RegionGroupId.Map.t) =
-  Some (ForwardEnd (ctx, loop_input_values, e, el))
+  ForwardEnd (ctx, loop_input_values, e, el)
 
 let synthesize_loop (loop_id : LoopId.id) (input_svalues : symbolic_value list)
     (fresh_svalues : SymbolicValueId.Set.t)
-    (rg_to_given_back_tys : ty list RegionGroupId.Map.t)
-    (end_expr : expression option) (loop_expr : expression option)
-    (span : Meta.span) : expression option =
-  match (end_expr, loop_expr) with
-  | None, None -> None
-  | Some end_expr, Some loop_expr ->
-      Some
-        (Loop
-           {
-             loop_id;
-             input_svalues;
-             fresh_svalues;
-             rg_to_given_back_tys;
-             end_expr;
-             loop_expr;
-             span;
-           })
-  | _ -> craise __FILE__ __LINE__ span "Unreachable"
-
-let save_snapshot (ctx : Contexts.eval_ctx) (e : expression option) :
-    expression option =
-  match e with None -> None | Some e -> Some (Meta (Snapshot ctx, e))
+    (rg_to_given_back_tys : ty list RegionGroupId.Map.t) (end_expr : expression)
+    (loop_expr : expression) (span : Meta.span) : expression =
+  Loop
+    {
+      loop_id;
+      input_svalues;
+      fresh_svalues;
+      rg_to_given_back_tys;
+      end_expr;
+      loop_expr;
+      span;
+    }
+
+let save_snapshot (ctx : Contexts.eval_ctx) (e : expression) : expression =
+  Meta (Snapshot ctx, e)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 02d495c0..0f887ec8 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -31,9 +31,8 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) :
   | None -> None
   | Some _ ->
       (* Evaluate *)
-      let synthesize = true in
-      let inputs, symb = evaluate_function_symbolic synthesize trans_ctx fdef in
-      Some (inputs, Option.get symb)
+      let inputs, symb = evaluate_function_symbolic trans_ctx fdef in
+      Some (inputs, symb)
 
 (** Translate a function, by generating its forward and backward translations.