diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index 6cccdce5a..fed120797 100644
--- a/sledge/src/control.ml
+++ b/sledge/src/control.ml
@@ -29,16 +29,13 @@ module Stack : sig
     -> t option
 
   val pop_return :
-       t
-    -> init:'a
-    -> f:(Var.t option -> Var.Set.t -> Domain.from_call -> 'a -> 'a)
-    -> (Llair.jump * 'a * t) option
+    t -> (Var.Set.t * Domain.from_call * Llair.jump * t) option
 
   val pop_throw :
        t
     -> init:'a
-    -> f:(Var.t option -> Var.Set.t -> Domain.from_call -> 'a -> 'a)
-    -> (Llair.jump * 'a * t) option
+    -> unwind:(Var.t list -> Var.Set.t -> Domain.from_call -> 'a -> 'a)
+    -> (Var.Set.t * Domain.from_call * Llair.jump * t * 'a) option
 end = struct
   type t =
     | Locals of Var.Set.t * t
@@ -46,8 +43,7 @@ end = struct
         { retreating: bool
               (** return from a call not known to be nonrecursive *)
         ; dst: Llair.Jump.t
-        ; freturn: Var.t option
-        ; fthrow: Var.t
+        ; params: Var.t list
         ; from_call: Domain.from_call
         ; stk: t }
     | Throw of Llair.Jump.t * t
@@ -112,16 +108,15 @@ end = struct
     (if Set.is_empty lcls then stk else Locals (lcls, stk))
     |> check invariant
 
-  let push_return ~retreating dst freturn fthrow from_call stk =
-    Return {retreating; dst; freturn; fthrow; from_call; stk}
-    |> check invariant
+  let push_return ~retreating dst params from_call stk =
+    Return {retreating; dst; params; from_call; stk} |> check invariant
 
   let push_throw jmp stk =
     (match jmp with None -> stk | Some jmp -> Throw (jmp, stk))
     |> check invariant
 
-  let push_call {Llair.locals; parent= {freturn; fthrow}} ~retreating ~bound
-      ~return from_call ?throw stk =
+  let push_call {Llair.params; locals} ~retreating ~bound ~return from_call
+      ?throw stk =
     [%Trace.call fun {pf} -> pf "%a" print_abbrev stk]
     ;
     let rec count_f_in_stack acc f = function
@@ -137,36 +132,28 @@ end = struct
       Some
         (push_jump locals
            (push_throw throw
-              (push_return ~retreating return freturn fthrow from_call stk)))
-    )
+              (push_return ~retreating return params from_call stk))) )
     |>
     [%Trace.retn fun {pf} _ ->
       pf "%d of %a on stack" n Llair.Jump.pp return]
 
-  let pop_return stk ~init ~f =
+  let pop_return stk =
     let rec pop_return_ scope = function
       | Locals (locals, stk) -> pop_return_ (Set.union locals scope) stk
       | Throw (_, stk) -> pop_return_ scope stk
-      | Return {dst; freturn; from_call; stk} ->
-          let dst =
-            match freturn with
-            | Some freturn -> {dst with args= Exp.var freturn :: dst.args}
-            | None -> dst
-          in
-          Some (dst, f freturn scope from_call init, stk)
+      | Return {from_call; dst; stk} -> Some (scope, from_call, dst, stk)
       | Empty -> None
     in
     pop_return_ Var.Set.empty stk
 
-  let pop_throw stk ~init ~f =
+  let pop_throw stk ~init ~unwind =
     let rec pop_throw_ scope state = function
       | Locals (locals, stk) ->
           pop_throw_ (Set.union locals scope) state stk
-      | Return {freturn; from_call; stk} ->
-          pop_throw_ Var.Set.empty (f freturn scope from_call state) stk
-      | Throw (dst, Return {fthrow; from_call; stk}) ->
-          let dst = {dst with args= Exp.var fthrow :: dst.args} in
-          Some (dst, f (Some fthrow) scope from_call state, stk)
+      | Return {params; from_call; stk} ->
+          pop_throw_ Var.Set.empty (unwind params scope from_call state) stk
+      | Throw (dst, Return {from_call; stk}) ->
+          Some (scope, from_call, dst, stk, state)
       | Empty -> None
       | Throw _ as stk -> violates invariant stk
     in
@@ -279,8 +266,8 @@ let exec_goto stk state block ({dst; retreating} : Llair.jump) =
   let stk = Stack.push_jump dst.locals stk in
   Work.add ~prev:block ~retreating stk state dst
 
-let exec_jump stk state block ({dst; args} as jmp : Llair.jump) =
-  let state = Domain.jump args dst.params dst.locals state in
+let exec_jump ?temps stk state block ({dst; args} as jmp : Llair.jump) =
+  let state = Domain.jump args dst.params dst.locals ?temps state in
   exec_goto stk state block jmp
 
 let exec_call ~opts stk state block ({dst; args; retreating} : Llair.jump)
@@ -299,20 +286,52 @@ let exec_call ~opts stk state block ({dst; args; retreating} : Llair.jump)
   |>
   [%Trace.retn fun {pf} _ -> pf ""]
 
-let exec_pop pop stk state (block : Llair.block) exp =
+let exec_return stk pre_state (block : Llair.block) exp =
   [%Trace.call fun {pf} -> pf "from %a" Var.pp block.parent.name.var]
   ;
-  ( match pop stk ~init:state ~f:(Domain.retn exp) with
-  | Some ((jmp : Llair.jump), state, stk) -> exec_jump stk state block jmp
+  ( match Stack.pop_return stk with
+  | Some (scope, from_call, retn_site, stk) ->
+      let freturn = block.parent.freturn in
+      let exit_state =
+        match (freturn, exp) with
+        | Some freturn, Some return_val ->
+            Domain.exec_return pre_state freturn return_val
+        | None, None -> pre_state
+        | _ -> violates Llair.Func.invariant block.parent
+      in
+      let post_state = Domain.post scope from_call exit_state in
+      let retn_state =
+        Domain.retn block.parent.entry.params from_call post_state
+      in
+      exec_jump stk retn_state block
+        ~temps:(Option.fold ~f:Set.add freturn ~init:Var.Set.empty)
+        ( match freturn with
+        | Some freturn -> Llair.Jump.push_arg (Exp.var freturn) retn_site
+        | None -> retn_site )
   | None -> Work.skip )
   |>
   [%Trace.retn fun {pf} _ -> pf ""]
 
-let exec_return stk state block exp =
-  exec_pop Stack.pop_return stk state block exp
-
-let exec_throw stk state block exc =
-  exec_pop Stack.pop_throw stk state block (Some exc)
+let exec_throw stk pre_state (block : Llair.block) exc =
+  [%Trace.call fun {pf} -> pf "from %a" Var.pp block.parent.name.var]
+  ;
+  let unwind params scope from_call state =
+    Domain.retn params from_call (Domain.post scope from_call state)
+  in
+  ( match Stack.pop_throw stk ~unwind ~init:pre_state with
+  | Some (scope, from_call, retn_site, stk, unwind_state) ->
+      let fthrow = block.parent.fthrow in
+      let exit_state = Domain.exec_return unwind_state fthrow exc in
+      let post_state = Domain.post scope from_call exit_state in
+      let retn_state =
+        Domain.retn block.parent.entry.params from_call post_state
+      in
+      exec_jump stk retn_state block
+        ~temps:(Set.add Var.Set.empty fthrow)
+        (Llair.Jump.push_arg (Exp.var fthrow) retn_site)
+  | None -> Work.skip )
+  |>
+  [%Trace.retn fun {pf} _ -> pf ""]
 
 let exec_skip_func :
     Stack.t -> Domain.t -> Llair.block -> Llair.jump -> Work.x =
@@ -342,12 +361,12 @@ let exec_term :
   | Switch {key; tbl; els} ->
       Vector.fold tbl
         ~f:(fun x (case, jump) ->
-          match Domain.assume state (Exp.eq key case) with
+          match Domain.exec_assume state (Exp.eq key case) with
           | Some state -> exec_jump stk state block jump |> Work.seq x
           | None -> x )
         ~init:
           ( match
-              Domain.assume state
+              Domain.exec_assume state
                 (Vector.fold tbl ~init:(Exp.bool true)
                    ~f:(fun b (case, _) -> Exp.and_ (Exp.dq key case) b))
             with
@@ -356,7 +375,7 @@ let exec_term :
   | Iswitch {ptr; tbl} ->
       Vector.fold tbl ~init:Work.skip ~f:(fun x (jump : Llair.jump) ->
           match
-            Domain.assume state
+            Domain.exec_assume state
               (Exp.eq ptr
                  (Exp.label
                     ~parent:(Var.name jump.dst.parent.name.var)
diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml
index 468d03c4b..87cb49021 100644
--- a/sledge/src/llair/llair.ml
+++ b/sledge/src/llair/llair.ml
@@ -276,6 +276,8 @@ module Jump = struct
   let mk lbl args =
     {dst= {dummy_block with lbl}; args; retreating= false}
     |> check invariant
+
+  let push_arg arg jmp = {jmp with args= arg :: jmp.args}
 end
 
 (** Basic-Block Terminators *)
@@ -285,7 +287,7 @@ module Term = struct
 
   let pp = pp_term
 
-  let invariant term =
+  let invariant ?parent term =
     Invariant.invariant [%here] term [%sexp_of: t]
     @@ fun () ->
     match term with
@@ -301,7 +303,12 @@ module Term = struct
             ~accept_return:(Option.is_some retn_typ && not ignore_result) ;
           Option.iter throw ~f:(Jump.invariant ~accept_return:true)
       | _ -> assert false )
-    | Return _ | Throw _ | Unreachable -> assert true
+    | Return {exp} -> (
+      match parent with
+      | Some parent ->
+          assert (Bool.(Option.is_some exp = Option.is_some parent.freturn))
+      | None -> assert true )
+    | Throw _ | Unreachable -> assert true
 
   let goto ~dst ~loc =
     Switch {key= Exp.bool false; tbl= Vector.empty; els= dst; loc}
@@ -318,14 +325,8 @@ module Term = struct
   let iswitch ~ptr ~tbl ~loc = Iswitch {ptr; tbl; loc} |> check invariant
 
   let call ~func ~typ ~args ~return ~throw ~ignore_result ~loc =
-    Call
-      { call= {dst= func; args; retreating= false}
-      ; typ
-      ; return
-      ; throw
-      ; ignore_result
-      ; loc }
-    |> check invariant
+    let call = {dst= func; args; retreating= false} in
+    Call {call; typ; return; throw; ignore_result; loc} |> check invariant
 
   let return ~exp ~loc = Return {exp; loc} |> check invariant
   let throw ~exc ~loc = Throw {exc; loc} |> check invariant
@@ -354,11 +355,7 @@ module Block = struct
 
   let mk ~lbl ~params ~cmnd ~term =
     let locals =
-      let locals_cmnd cmnd vs =
-        Vector.fold_right cmnd ~init:vs ~f:Inst.union_locals
-      in
-      let locals_params params vs = List.fold params ~init:vs ~f:Set.add in
-      locals_params params (locals_cmnd cmnd Var.Set.empty)
+      Vector.fold_right ~f:Inst.union_locals cmnd ~init:Var.Set.empty
     in
     { lbl
     ; params
@@ -408,7 +405,7 @@ module Func = struct
     assert (func == func.entry.parent) ;
     let {name= {typ}; cfg} = func in
     match typ with
-    | Pointer _ ->
+    | Pointer {elt= Function {return}} ->
         assert (
           not
             (Vector.contains_dup cfg ~compare:(fun b1 b2 ->
@@ -419,7 +416,8 @@ module Func = struct
                (List.concat_map (Vector.to_list cfg) ~f:(fun {params} ->
                     params ))
                ~compare:Var.compare) ) ;
-        iter_term func ~f:(fun term -> Term.invariant term)
+        assert (Bool.(Option.is_some return = Option.is_some func.freturn)) ;
+        iter_term func ~f:(fun term -> Term.invariant ~parent:func term)
     | _ -> assert false
 
   let find functions name = Map.find functions name
@@ -427,21 +425,18 @@ module Func = struct
   let mk ~(name : Global.t) ~entry ~cfg =
     let locals =
       Vector.fold ~init:entry.locals cfg ~f:(fun locals block ->
-          Set.union locals block.locals )
+          Set.add_list block.params (Set.union locals block.locals) )
     in
-    let freturn, locals =
+    let entry = {entry with locals} in
+    let wrt = Set.add_list entry.params locals in
+    let freturn, wrt =
       match name.typ with
       | Pointer {elt= Function {return= Some _}} ->
-          let freturn, locals =
-            Var.fresh "freturn" ~wrt:(Set.add_list entry.params locals)
-          in
-          (Some freturn, locals)
-      | _ -> (None, locals)
-    in
-    let fthrow, locals =
-      Var.fresh "fthrow" ~wrt:(Set.add_list entry.params locals)
+          let freturn, wrt = Var.fresh "freturn" ~wrt in
+          (Some freturn, wrt)
+      | _ -> (None, wrt)
     in
-    let entry = {entry with locals} in
+    let fthrow, _ = Var.fresh "fthrow" ~wrt in
     let func = {name; entry; cfg; freturn; fthrow} in
     let resolve_parent_and_jumps block =
       block.parent <- func ;
diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli
index 08600bb3f..5dfa78fda 100644
--- a/sledge/src/llair/llair.mli
+++ b/sledge/src/llair/llair.mli
@@ -95,7 +95,7 @@ and term = private
 and block = private
   { lbl: label
   ; params: Var.t list  (** Formal parameters, first-param-last stack *)
-  ; locals: Var.Set.t  (** Local variables, including [params]. *)
+  ; locals: Var.Set.t  (** Local variables *)
   ; cmnd: cmnd
   ; term: term
   ; mutable parent: func
@@ -148,6 +148,7 @@ module Jump : sig
 
   val pp : jump pp
   val mk : string -> Exp.t list -> jump
+  val push_arg : Exp.t -> jump -> jump
 end
 
 module Term : sig
diff --git a/sledge/src/symbheap/domain.ml b/sledge/src/symbheap/domain.ml
index 7a33722d9..39fbbdeeb 100644
--- a/sledge/src/symbheap/domain.ml
+++ b/sledge/src/symbheap/domain.ml
@@ -21,8 +21,8 @@ let join (entry_a, current_a) (entry_b, current_b) =
   assert (State_domain.equal entry_b entry_a) ;
   (entry_a, State_domain.join current_a current_b)
 
-let assume (entry, current) q =
-  match State_domain.assume current q with
+let exec_assume (entry, current) cnd =
+  match State_domain.exec_assume current cnd with
   | Some current -> Some (entry, current)
   | None -> None
 
@@ -31,6 +31,9 @@ let exec_inst (entry, current) inst =
   | Ok current -> Ok (entry, current)
   | Error e -> Error e
 
+let exec_return (entry, current) formal actual =
+  (entry, State_domain.exec_return current formal actual)
+
 let exec_intrinsic (entry, current) result intrinsic actuals =
   match State_domain.exec_intrinsic current result intrinsic actuals with
   | None -> None
@@ -41,8 +44,10 @@ type from_call =
   {state_from_call: State_domain.from_call; caller_entry: State_domain.t}
 [@@deriving sexp_of]
 
-let jump actuals formals locals (entry, current) =
-  let current, _ = State_domain.call actuals formals locals current in
+let jump actuals formals locals ?temps (entry, current) =
+  let current, _ =
+    State_domain.call actuals formals locals ?temps current
+  in
   (entry, current)
 
 let call actuals formals locals (_, current) =
@@ -55,11 +60,17 @@ let call actuals formals locals (_, current) =
   |>
   [%Trace.retn fun {pf} (reln, _) -> pf "@,%a" pp reln]
 
-let retn actual formal locals {caller_entry; state_from_call} (_, current) =
+let post locals {caller_entry} (_, current) =
+  [%Trace.call fun {pf} -> pf ""]
+  ;
+  (caller_entry, State_domain.post locals current)
+  |>
+  [%Trace.retn fun {pf} -> pf "@,%a" pp]
+
+let retn formals {caller_entry; state_from_call} (_, current) =
   [%Trace.call fun {pf} -> pf ""]
   ;
-  ( caller_entry
-  , State_domain.retn actual formal locals state_from_call current )
+  (caller_entry, State_domain.retn formals state_from_call current)
   |>
   [%Trace.retn fun {pf} -> pf "@,%a" pp]
 
diff --git a/sledge/src/symbheap/domain.mli b/sledge/src/symbheap/domain.mli
index 1d53cc355..f9b4cca65 100644
--- a/sledge/src/symbheap/domain.mli
+++ b/sledge/src/symbheap/domain.mli
@@ -12,17 +12,21 @@ type t
 val pp : t pp
 val init : Global.t vector -> t
 val join : t -> t -> t
-val assume : t -> Exp.t -> t option
+val exec_assume : t -> Exp.t -> t option
 val exec_inst : t -> Llair.inst -> (t, unit) result
+val exec_return : t -> Var.t -> Exp.t -> t
 
 val exec_intrinsic :
   t -> Var.t option -> Var.t -> Exp.t list -> (t, unit) result option
 
 type from_call [@@deriving sexp_of]
 
-val jump : Exp.t list -> Var.t list -> Var.Set.t -> t -> t
+val jump :
+  Exp.t list -> Var.t list -> Var.Set.t -> ?temps:Var.Set.t -> t -> t
+
 val call : Exp.t list -> Var.t list -> Var.Set.t -> t -> t * from_call
-val retn : Exp.t option -> Var.t option -> Var.Set.t -> from_call -> t -> t
+val post : Var.Set.t -> from_call -> t -> t
+val retn : Var.t list -> from_call -> t -> t
 
 val resolve_callee :
   (Var.t -> Llair.func list) -> Exp.t -> t -> Llair.func list
diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml
index e2d8318f6..7ea7650ca 100644
--- a/sledge/src/symbheap/exec.ml
+++ b/sledge/src/symbheap/exec.ml
@@ -33,7 +33,9 @@ let zero = Exp.integer Z.zero Typ.siz
  * Instruction small axioms
  *)
 
-let assume cnd pre =
+let return pre formal exp = Sh.and_ (Exp.eq (Exp.var formal) exp) pre
+
+let assume pre cnd =
   let post = Sh.and_ cnd pre in
   if Sh.is_false post then None else Some post
 
diff --git a/sledge/src/symbheap/exec.mli b/sledge/src/symbheap/exec.mli
index 045094525..715777120 100644
--- a/sledge/src/symbheap/exec.mli
+++ b/sledge/src/symbheap/exec.mli
@@ -7,7 +7,8 @@
 
 (** Symbolic Execution *)
 
-val assume : Exp.t -> Sh.t -> Sh.t option
+val assume : Sh.t -> Exp.t -> Sh.t option
+val return : Sh.t -> Var.t -> Exp.t -> Sh.t
 val inst : Sh.t -> Llair.inst -> (Sh.t, unit) result
 
 val intrinsic :
diff --git a/sledge/src/symbheap/state_domain.ml b/sledge/src/symbheap/state_domain.ml
index a58ff7c91..b609f8415 100644
--- a/sledge/src/symbheap/state_domain.ml
+++ b/sledge/src/symbheap/state_domain.ml
@@ -13,10 +13,6 @@ let pp_full fs s = [%Trace.fprintf fs "%a" Sh.pp s]
 let pp fs s = [%Trace.fprintf fs "%a" Sh.pp (Sh.simplify s)]
 let pp fs s = pp_full fs s ; pp fs s
 
-(* I think it would be nice if `-t State_domain.pp` enabled the simplified
-   printing, with `-t State_domain.pp_full` for the more verbose one. So how
-   about this renaming? *)
-
 let init globals =
   Vector.fold globals ~init:Sh.emp ~f:(fun q -> function
     | {Global.var; init= Some (arr, siz)} ->
@@ -26,7 +22,8 @@ let init globals =
     | _ -> q )
 
 let join = Sh.or_
-let assume q b = Exec.assume b q
+let exec_assume = Exec.assume
+let exec_return = Exec.return
 let exec_inst = Exec.inst
 let exec_intrinsic = Exec.intrinsic
 
@@ -34,15 +31,17 @@ type from_call = Var.Subst.t [@@deriving compare, equal, sexp]
 
 (** Express formula in terms of formals instead of actuals, and enter scope
     of locals: rename formals to fresh vars in formula and actuals, add
-    equations between each formal and actual, and quantify the fresh vars. *)
-let call actuals formals locals q =
+    equations between each formal and actual, and quantify the temps and
+    fresh vars. *)
+let call actuals formals locals ?temps q =
   [%Trace.call fun {pf} ->
     pf
       "@[<hv>actuals: (@[%a@])@ formals: (@[%a@])@ locals: {@[%a@]}@ q: %a@]"
       (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp)
       (List.rev formals) Var.Set.pp locals Sh.pp q]
   ;
-  let q', freshen_locals = Sh.freshen q ~wrt:locals in
+  let wrt = Set.add_list formals locals in
+  let q', freshen_locals = Sh.freshen q ~wrt in
   let and_eq q formal actual =
     let actual' = Exp.rename actual freshen_locals in
     Sh.and_ (Exp.eq (Exp.var formal) actual') q
@@ -50,33 +49,36 @@ let call actuals formals locals q =
   let and_eqs formals actuals q =
     List.fold2_exn ~f:and_eq formals actuals ~init:q
   in
-  (Sh.extend_us locals (and_eqs formals actuals q'), freshen_locals)
+  ( Sh.extend_us locals
+      (Option.fold ~f:(Fn.flip Sh.exists) temps
+         ~init:(and_eqs formals actuals q'))
+  , freshen_locals )
   |>
   [%Trace.retn fun {pf} (q', s) ->
     pf "@[<hv>subst: %a@ q': %a@]" Var.Subst.pp s Sh.pp q']
 
-(** Leave scope of locals and express in terms of actuals instead of
-    formals: existentially quantify locals and formals, and apply inverse of
-    fresh variables for formals renaming to restore the shadowed variables. *)
-let retn actual formal locals freshen_locals q =
+(** Leave scope of locals: existentially quantify locals. *)
+let post locals q =
   [%Trace.call fun {pf} ->
-    pf "@[<hv>%a%alocals: {@[%a@]}@ subst: %a@ q: %a@]"
-      (Option.pp "%a to " Exp.pp)
-      actual (Option.pp "%a@ " Var.pp) formal Var.Set.pp locals Var.Subst.pp
+    pf "@[<hv>locals: {@[%a@]}@ q: %a@]" Var.Set.pp locals Sh.pp q]
+  ;
+  Sh.exists locals q
+  |>
+  [%Trace.retn fun {pf} -> pf "%a" Sh.pp]
+
+(** Express in terms of actuals instead of formals: existentially quantify
+    formals, and apply inverse of fresh variables for formals renaming to
+    restore the shadowed variables. *)
+let retn formals freshen_locals q =
+  [%Trace.call fun {pf} ->
+    pf "@[<hv>formals: {@[%a@]}@ subst: %a@ q: %a@]" (List.pp ", " Var.pp)
+      formals Var.Subst.pp
       (Var.Subst.invert freshen_locals)
       Sh.pp q]
   ;
-  let q' =
-    match (actual, formal) with
-    | Some actl, Some frml -> Sh.and_ (Exp.eq (Exp.var frml) actl) q
-    | None, None -> q
-    | _ ->
-        fail "mismatched actual and formal return: %a to %a"
-          (Option.pp "%a" Exp.pp) actual (Option.pp "%a" Var.pp) formal ()
-  in
   Sh.rename
     (Var.Subst.invert freshen_locals)
-    (Sh.exists (Option.fold ~f:Set.remove ~init:locals formal) q')
+    (Sh.exists (Var.Set.of_list formals) q)
   |>
   [%Trace.retn fun {pf} -> pf "%a" Sh.pp]
 
diff --git a/sledge/src/symbheap/state_domain.mli b/sledge/src/symbheap/state_domain.mli
index 61e850688..194e8b4a3 100644
--- a/sledge/src/symbheap/state_domain.mli
+++ b/sledge/src/symbheap/state_domain.mli
@@ -12,16 +12,25 @@ type t [@@deriving equal, sexp_of]
 val pp : t pp
 val init : Global.t vector -> t
 val join : t -> t -> t
-val assume : t -> Exp.t -> t option
+val exec_assume : t -> Exp.t -> t option
 val exec_inst : t -> Llair.inst -> (t, unit) result
+val exec_return : t -> Var.t -> Exp.t -> t
 
 val exec_intrinsic :
   t -> Var.t option -> Var.t -> Exp.t list -> (t, unit) result option
 
 type from_call [@@deriving compare, equal, sexp]
 
-val call : Exp.t list -> Var.t list -> Var.Set.t -> t -> t * from_call
-val retn : Exp.t option -> Var.t option -> Var.Set.t -> from_call -> t -> t
+val call :
+     Exp.t list
+  -> Var.t list
+  -> Var.Set.t
+  -> ?temps:Var.Set.t
+  -> t
+  -> t * from_call
+
+val post : Var.Set.t -> t -> t
+val retn : Var.t list -> from_call -> t -> t
 
 val resolve_callee :
   (Var.t -> Llair.func list) -> Exp.t -> t -> Llair.func list