diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index 47f110303..b3dadf0d1 100644
--- a/sledge/src/control.ml
+++ b/sledge/src/control.ml
@@ -18,14 +18,7 @@ module Stack : sig
   val empty : t
 
   val push_call :
-       Llair.block
-    -> retreating:bool
-    -> bound:int
-    -> return:Llair.jump
-    -> Domain.from_call
-    -> ?throw:Llair.jump
-    -> t
-    -> t option
+    Llair.func Llair.call -> bound:int -> Domain.from_call -> t -> t option
 
   val pop_return : t -> (Domain.from_call * Llair.jump * t) option
 
@@ -37,8 +30,7 @@ module Stack : sig
 end = struct
   type t =
     | Return of
-        { retreating: bool
-              (** return from a call not known to be nonrecursive *)
+        { recursive: bool  (** return from a possibly-recursive call *)
         ; dst: Llair.Jump.t
         ; params: Var.t list
         ; locals: Var.Set.t
@@ -59,8 +51,8 @@ end = struct
     if x == y then 0
     else
       match (x, y) with
-      | Return {retreating= true; stk= x}, y
-       |x, Return {retreating= true; stk= y} ->
+      | Return {recursive= true; stk= x}, y
+       |x, Return {recursive= true; stk= y} ->
           compare_as_inlined_location x y
       | Return {dst= j; stk= x}, Return {dst= k; stk= y} -> (
         match Llair.Jump.compare j k with
@@ -77,10 +69,10 @@ end = struct
       | Empty, Empty -> 0
 
   let rec print_abbrev fs = function
-    | Return {retreating= false; stk= s} ->
+    | Return {recursive= false; stk= s} ->
         print_abbrev fs s ;
         Format.pp_print_char fs 'R'
-    | Return {retreating= true; stk= s} ->
+    | Return {recursive= true; stk= s} ->
         print_abbrev fs s ;
         Format.pp_print_string fs "R↑"
     | Throw (_, s) ->
@@ -97,16 +89,16 @@ end = struct
 
   let empty = Empty |> check invariant
 
-  let push_return ~retreating dst params locals from_call stk =
-    Return {retreating; dst; params; locals; from_call; stk}
+  let push_return Llair.{callee= {params; locals}; return; recursive}
+      from_call stk =
+    Return {recursive; dst= return; params; locals; 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 (entry : Llair.block) ~retreating ~bound ~return from_call
-      ?throw stk =
+  let push_call (Llair.{return; throw} as call) ~bound from_call stk =
     [%Trace.call fun {pf} -> pf "%a" print_abbrev stk]
     ;
     let rec count_f_in_stack acc f = function
@@ -118,11 +110,7 @@ end = struct
     in
     let n = count_f_in_stack 0 return stk in
     ( if n > bound then None
-    else
-      Some
-        (push_throw throw
-           (push_return ~retreating return entry.params entry.parent.locals
-              from_call stk)) )
+    else Some (push_throw throw (push_return call from_call stk)) )
     |>
     [%Trace.retn fun {pf} _ ->
       pf "%d of %a on stack" n Llair.Jump.pp return]
@@ -246,55 +234,52 @@ end = struct
     | None -> [%Trace.info "queue empty"] ; ()
 end
 
-let exec_goto stk state block ({dst; retreating} : Llair.jump) =
+let exec_jump stk state block Llair.{dst; retreating} =
   Work.add ~prev:block ~retreating stk state dst
 
-let exec_jump ?temps stk state block ({dst; args} as jmp : Llair.jump) =
-  let state = Domain.jump args dst.params ?temps state in
-  exec_goto stk state block jmp
-
 let summary_table = Hashtbl.create (module Var)
 
-let exec_call opts stk state block ({dst; args; retreating} : Llair.jump)
-    (return : Llair.jump) throw globals =
+let exec_call opts stk state block call globals =
+  let Llair.{callee; args; areturn; return; recursive} = call in
+  let Llair.{name; params; freturn; locals; entry} = callee in
   [%Trace.call fun {pf} ->
-    pf "%a from %a" Var.pp dst.parent.name.var Var.pp
-      return.dst.parent.name.var]
+    pf "%a from %a" Var.pp name.var Var.pp return.dst.parent.name.var]
   ;
   let dnf_states =
     if opts.function_summaries then Domain.dnf state else [state]
   in
-  let locals = dst.parent.locals in
-  let domain_call = Domain.call args dst.params locals globals in
+  let domain_call =
+    Domain.call args areturn params (Set.add_option freturn locals) globals
+  in
   List.fold ~init:Work.skip dnf_states ~f:(fun acc state ->
-      let maybe_summary_post =
-        if opts.function_summaries then
-          let state = fst (domain_call ~summaries:false state) in
-          Hashtbl.find summary_table dst.parent.name.var
-          >>= List.find_map ~f:(Domain.apply_summary state)
-        else None
-      in
-      [%Trace.info
-        "Maybe summary post: %a"
-          (Option.pp "%a" Domain.pp)
-          maybe_summary_post] ;
-      match maybe_summary_post with
+      match
+        if not opts.function_summaries then None
+        else
+          let maybe_summary_post =
+            let state = fst (domain_call ~summaries:false state) in
+            Hashtbl.find summary_table name.var
+            >>= List.find_map ~f:(Domain.apply_summary state)
+          in
+          [%Trace.info
+            "Maybe summary post: %a"
+              (Option.pp "%a" Domain.pp)
+              maybe_summary_post] ;
+          maybe_summary_post
+      with
       | None ->
           let state, from_call =
             domain_call ~summaries:opts.function_summaries state
           in
           Work.seq acc
-            ( match
-                Stack.push_call ~bound:opts.bound dst ~retreating ~return
-                  from_call ?throw stk
-              with
-            | Some stk -> Work.add stk ~prev:block ~retreating state dst
+            ( match Stack.push_call call ~bound:opts.bound from_call stk with
+            | Some stk ->
+                Work.add stk ~prev:block ~retreating:recursive state entry
             | None -> Work.skip )
-      | Some post -> Work.seq acc (exec_goto stk post block return) )
+      | Some post -> Work.seq acc (exec_jump stk post block return) )
   |>
   [%Trace.retn fun {pf} _ -> pf ""]
 
-let pp_st _ =
+let pp_st () =
   [%Trace.printf
     "@[<v>%t@]" (fun fs ->
         Hashtbl.iteri summary_table ~f:(fun ~key ~data ->
@@ -303,88 +288,72 @@ let pp_st _ =
               data ) )]
 
 let exec_return ~opts stk pre_state (block : Llair.block) exp globals =
-  [%Trace.call fun {pf} -> pf "from %a" Var.pp block.parent.name.var]
+  let Llair.{name; params; freturn; locals} = block.parent in
+  [%Trace.call fun {pf} -> pf "from %a" Var.pp name.var]
   ;
   ( match Stack.pop_return stk with
   | Some (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
+            Domain.exec_move pre_state freturn return_val
         | None, None -> pre_state
         | _ -> violates Llair.Func.invariant block.parent
       in
-      let exit_state =
+      let post_state = Domain.post locals from_call exit_state in
+      let post_state =
         if opts.function_summaries then (
           let globals =
             Var.Set.of_vector
               (Vector.map globals ~f:(fun (g : Global.t) -> g.var))
           in
-          let function_summary, exit_state =
-            Domain.create_summary ~locals:block.parent.locals exit_state
-              ~formals:
-                (Set.union
-                   (Var.Set.of_list block.parent.entry.params)
-                   globals)
+          let function_summary, post_state =
+            Domain.create_summary ~locals post_state
+              ~formals:(Set.union (Var.Set.of_list params) globals)
           in
-          Hashtbl.add_multi summary_table ~key:block.parent.name.var
+          Hashtbl.add_multi summary_table ~key:name.var
             ~data:function_summary ;
           pp_st () ;
-          exit_state )
-        else exit_state
+          post_state )
+        else post_state
       in
-      let post_state =
-        Domain.post block.parent.locals 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 )
+      let retn_state = Domain.retn params freturn from_call post_state in
+      exec_jump stk retn_state block retn_site
   | None -> Work.skip )
   |>
   [%Trace.retn fun {pf} _ -> pf ""]
 
 let exec_throw stk pre_state (block : Llair.block) exc =
-  [%Trace.call fun {pf} -> pf "from %a" Var.pp block.parent.name.var]
+  let func = block.parent in
+  [%Trace.call fun {pf} -> pf "from %a" Var.pp func.name.var]
   ;
   let unwind params scope from_call state =
-    Domain.retn params from_call (Domain.post scope from_call state)
+    Domain.retn params (Some func.fthrow) from_call
+      (Domain.post scope from_call state)
   in
   ( match Stack.pop_throw stk ~unwind ~init:pre_state with
   | Some (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 block.parent.locals from_call exit_state
-      in
+      let fthrow = func.fthrow in
+      let exit_state = Domain.exec_move unwind_state fthrow exc in
+      let post_state = Domain.post func.locals from_call exit_state in
       let retn_state =
-        Domain.retn block.parent.entry.params from_call post_state
+        Domain.retn func.params func.freturn 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)
+      exec_jump stk retn_state block retn_site
   | None -> Work.skip )
   |>
   [%Trace.retn fun {pf} _ -> pf ""]
 
 let exec_skip_func :
-    Stack.t -> Domain.t -> Llair.block -> Llair.jump -> Work.x =
- fun stk state block ({dst; args} as return) ->
+       Stack.t
+    -> Domain.t
+    -> Llair.block
+    -> Var.t option
+    -> Llair.jump
+    -> Work.x =
+ fun stk state block areturn return ->
   Report.unknown_call block.term ;
-  let return =
-    if List.is_empty dst.params then return
-    else
-      let args =
-        List.fold_right dst.params ~init:args ~f:(fun param args ->
-            Exp.nondet (Var.name param) :: args )
-      in
-      {return with args}
-  in
+  let state = Option.fold ~f:Domain.exec_kill ~init:state areturn in
   exec_jump stk state block return
 
 let exec_term :
@@ -417,32 +386,30 @@ let exec_term :
           with
           | Some state -> exec_jump stk state block jump |> Work.seq x
           | None -> x )
-  | Call {call= {dst; args; retreating}; return; throw} -> (
+  | Call ({callee; args; areturn; return} as call) -> (
     match
       let lookup name =
         Option.to_list (Llair.Func.find pgm.functions name)
       in
-      Domain.resolve_callee lookup dst state
+      Domain.resolve_callee lookup callee state
     with
-    | [] -> exec_skip_func stk state block return
+    | [] -> exec_skip_func stk state block areturn return
     | callees ->
         List.fold callees ~init:Work.skip ~f:(fun x callee ->
             ( match
                 Domain.exec_intrinsic ~skip_throw:opts.skip_throw state
-                  (List.hd return.dst.params)
-                  callee.name.var args
+                  areturn callee.name.var args
               with
             | Some (Error ()) ->
                 Report.invalid_access_term (Domain.project state) block.term ;
                 Work.skip
             | Some (Ok state) when Domain.is_false state -> Work.skip
-            | Some (Ok state) -> exec_goto stk state block return
+            | Some (Ok state) -> exec_jump stk state block return
             | None when Llair.Func.is_undefined callee ->
-                exec_skip_func stk state block return
+                exec_skip_func stk state block areturn return
             | None ->
-                exec_call opts stk state block
-                  {dst= callee.entry; args; retreating}
-                  return throw pgm.globals )
+                exec_call opts stk state block {call with callee}
+                  pgm.globals )
             |> Work.seq x ) )
   | Return {exp} -> exec_return ~opts stk state block exp pgm.globals
   | Throw {exc} ->
@@ -471,13 +438,13 @@ let harness : exec_opts -> Llair.t -> (int -> Work.t) option =
   List.find_map entry_points ~f:(fun name ->
       Llair.Func.find pgm.functions (Var.program name) )
   |> function
-  | Some {locals; entry= {params= []} as block} ->
+  | Some {locals; params= []; entry} ->
       Some
         (Work.init
            (fst
-              (Domain.call ~summaries:opts.function_summaries [] [] locals
-                 pgm.globals (Domain.init pgm.globals)))
-           block)
+              (Domain.call ~summaries:opts.function_summaries [] None []
+                 locals pgm.globals (Domain.init pgm.globals)))
+           entry)
   | _ -> None
 
 let exec_pgm : exec_opts -> Llair.t -> unit =
diff --git a/sledge/src/import/import.ml b/sledge/src/import/import.ml
index 32467f953..f28876b77 100644
--- a/sledge/src/import/import.ml
+++ b/sledge/src/import/import.ml
@@ -264,6 +264,7 @@ module Set = struct
   let equal_m__t (module Elt : Compare_m) = equal
   let pp pp_elt fs x = List.pp ",@ " pp_elt fs (to_list x)
   let disjoint x y = is_empty (inter x y)
+  let add_option yo x = Option.fold ~f:add ~init:x yo
   let add_list ys x = List.fold ~f:add ~init:x ys
   let diff_inter_diff x y = (diff x y, inter x y, diff y x)
   let inter_diff x y = (inter x y, diff y x)
diff --git a/sledge/src/import/import.mli b/sledge/src/import/import.mli
index 18cf60a39..0d80c9536 100644
--- a/sledge/src/import/import.mli
+++ b/sledge/src/import/import.mli
@@ -212,6 +212,7 @@ module Set : sig
 
   val pp : 'e pp -> ('e, 'c) t pp
   val disjoint : ('e, 'c) t -> ('e, 'c) t -> bool
+  val add_option : 'e option -> ('e, 'c) t -> ('e, 'c) t
   val add_list : 'e list -> ('e, 'c) t -> ('e, 'c) t
 
   val diff_inter_diff :
diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index c9c01dc5e..08b3d58eb 100644
--- a/sledge/src/llair/exp.ml
+++ b/sledge/src/llair/exp.ml
@@ -520,6 +520,7 @@ module Var = struct
     let pp_full ?is_x vs = Set.pp (pp_full ?is_x) vs
     let pp = pp_full ?is_x:None
     let empty = Set.empty (module T)
+    let of_option = Option.fold ~f:Set.add ~init:empty
     let of_list = Set.of_list (module T)
     let of_vector = Set.of_vector (module T)
   end
diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli
index f8070f81b..a7edf4a6d 100644
--- a/sledge/src/llair/exp.mli
+++ b/sledge/src/llair/exp.mli
@@ -99,6 +99,7 @@ module Var : sig
     val pp_full : ?is_x:(exp -> bool) -> t pp
     val pp : t pp
     val empty : t
+    val of_option : var option -> t
     val of_list : var list -> t
     val of_vector : var vector -> t
   end
diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml
index 5a8243c07..ae8b8d6de 100644
--- a/sledge/src/llair/frontend.ml
+++ b/sledge/src/llair/frontend.ml
@@ -675,150 +675,49 @@ let landingpad_typs : x -> Llvm.llvalue -> Typ.t * Typ.t * Llvm.lltype =
   let cxa_exception = Llvm.struct_type llcontext [|tip; dtor|] in
   (i32, xlate_type x tip, cxa_exception)
 
-(** construct the argument of a landingpad block, mainly fix the encoding
-    scheme for landingpad instruction name to block arg name *)
-let landingpad_arg : Llvm.llvalue -> Var.t =
- fun instr -> Var.program (find_name instr ^ ".exc")
-
-(** [rev_map_phis ~f blk] returns [(retn_arg, rev_args, pos)] by rev_mapping
-    over the prefix of [PHI] instructions at the beginning of [blk].
-    [retn_arg], if any, is [f] applied to the [PHI] instruction which takes
-    the return value of every [Invoke] predecessor of [blk]. [rev_args] is
-    the result of applying [f] to each of the other [PHI] instructions.
-    [pos] is the instruction iterator position before the first non-[PHI]
-    instruction of [blk]. *)
-let rev_map_phis :
-       f:(Llvm.llvalue -> 'a)
+(** Translate a control transfer from instruction [instr] to block [dst] to
+    a jump, if necessary by extending [blocks] with a trampoline containing
+    the PHIs of [dst] translated to a move. *)
+let xlate_jump :
+       x
+    -> ?reg_exps:(Var.var * Exp.t) list
+    -> Llvm.llvalue
     -> Llvm.llbasicblock
-    -> 'a option * 'a list * _ Llvm.llpos =
- fun ~f blk ->
-  let rec block_args_ found_invoke_pred retn_arg rev_args pos =
-    match (pos : _ Llvm.llpos) with
-    | Before instr -> (
-      match Llvm.instr_opcode instr with
+    -> Loc.t
+    -> Llair.block list
+    -> Llair.jump * Llair.block list =
+ fun x ?(reg_exps = []) instr dst loc blocks ->
+  let src = Llvm.instr_parent instr in
+  let rec xlate_jump_ reg_exps (pos : _ Llvm.llpos) =
+    match pos with
+    | Before dst_instr -> (
+      match Llvm.instr_opcode dst_instr with
       | PHI ->
-          (* [has_invoke_pred] holds if some value selected by this PHI is
-             the return value of an [invoke] instr. [is_retn_arg] holds if
-             for each predecessor terminated by an invoke instr, this PHI
-             instr takes the value of the invoke's return value. *)
-          let has_invoke_pred, is_retn_arg =
-            List.fold (Llvm.incoming instr) ~init:(false, true)
-              ~f:(fun (has_invoke_pred, is_retn_arg) (arg, pred) ->
-                match Llvm.block_terminator pred with
-                | Some instr -> (
-                  match Llvm.instr_opcode instr with
-                  | Invoke when Poly.equal arg instr -> (true, is_retn_arg)
-                  | Invoke -> (has_invoke_pred, false)
-                  | _ -> (has_invoke_pred, is_retn_arg) )
-                | None -> fail "rev_map_phis: %a" pp_llblock blk () )
-          in
-          if found_invoke_pred && has_invoke_pred then
-            (* Supporting multiple PHI instructions that take the return
-               values of invoke instructions will require adding trampolines
-               for the invoke instructions to return to, that each reorder
-               arguments and invoke the translation of this block. *)
-            todo "multiple PHI instructions taking invoke return values: %a"
-              pp_llblock blk () ;
-          let retn_arg, rev_args =
-            if has_invoke_pred && is_retn_arg then (Some (f instr), rev_args)
-            else (None, f instr :: rev_args)
+          let reg_exp =
+            List.find_map_exn (Llvm.incoming dst_instr)
+              ~f:(fun (arg, pred) ->
+                if Poly.equal pred src then
+                  Some (xlate_name dst_instr, xlate_value x arg)
+                else None )
           in
-          block_args_ has_invoke_pred retn_arg rev_args
-            (Llvm.instr_succ instr)
-      | LandingPad when Option.is_some retn_arg ->
-          (* Supporting returning and throwing to the same block, with
-             different arguments, will require adding trampolines. *)
-          todo
-            "return and throw to the same block with different arguments: %a"
-            pp_llblock blk ()
-      | _ -> (retn_arg, rev_args, pos) )
-    | At_end blk -> fail "rev_map_phis: %a" pp_llblock blk ()
+          xlate_jump_ (reg_exp :: reg_exps) (Llvm.instr_succ dst_instr)
+      | _ -> reg_exps )
+    | At_end blk -> fail "xlate_jump: %a" pp_llblock blk ()
   in
-  block_args_ false None [] (Llvm.instr_begin blk)
-
-(** [trampoline_args jump_instr dest_block] is the actual arguments to which
-    the translation of [dest_block] should be partially-applied, to yield a
-    trampoline accepting the return parameter of the block and then jumping
-    with all the args. *)
-let trampoline_args : x -> Llvm.llvalue -> Llvm.llbasicblock -> Exp.t list =
- fun x jmp dst ->
-  let src = Llvm.instr_parent jmp in
-  rev_map_phis dst ~f:(fun instr ->
-      List.find_map_exn (Llvm.incoming instr) ~f:(fun (arg, pred) ->
-          if Poly.equal pred src then Some (xlate_value x arg) else None )
-  )
-  |> snd3
-
-(** [unique_pred blk] is the unique predecessor of [blk], or [None] if there
-    are 0 or >1 predecessors. *)
-let unique_pred : Llvm.llbasicblock -> Llvm.llvalue option =
- fun blk ->
-  match Llvm.use_begin (Llvm.value_of_block blk) with
-  | Some use -> (
-    match Llvm.use_succ use with
-    | None -> Some (Llvm.user use)
-    | Some _ -> None )
-  | None -> None
-
-(** [return_formal_is_used instr] holds if the return value of [instr] is
-    used anywhere. *)
-let return_formal_is_used : Llvm.llvalue -> bool =
- fun instr -> Option.is_some (Llvm.use_begin instr)
-
-(** [need_return_trampoline instr blk] holds when the return formal of
-    [instr] is used, but the returned to block [blk] does not take it as an
-    argument (e.g. if it has multiple predecessors and no PHI node). *)
-let need_return_trampoline : Llvm.llvalue -> Llvm.llbasicblock -> bool =
- fun instr blk ->
-  Option.is_none (fst3 (rev_map_phis blk ~f:Fn.id))
-  && Option.is_none (unique_pred blk)
-  && return_formal_is_used instr
-
-(** [unique_used_invoke_pred blk] is the unique predecessor of [blk], if it
-    is an [Invoke] instruction, whose return value is used. *)
-let unique_used_invoke_pred : Llvm.llbasicblock -> 'a option =
- fun blk ->
-  let is_invoke i = Poly.equal (Llvm.instr_opcode i) Invoke in
-  match unique_pred blk with
-  | Some instr when is_invoke instr && return_formal_is_used instr ->
-      Some instr
-  | _ -> None
-
-(** formal parameters accepted by a block *)
-let block_formals : Llvm.llbasicblock -> Var.t list * _ Llvm.llpos =
- fun blk ->
-  let retn_arg, rev_args, pos = rev_map_phis blk ~f:xlate_name in
-  match pos with
-  | Before instr ->
-      let instr_arg =
-        match Llvm.instr_opcode instr with
-        | LandingPad ->
-            assert (Option.is_none retn_arg (* ensured by rev_map_phis *)) ;
-            Some (landingpad_arg instr)
-        | _ ->
-            Option.first_some retn_arg
-              (Option.map (unique_used_invoke_pred blk) ~f:xlate_name)
+  let jmp = Llair.Jump.mk (label_of_block dst) in
+  match xlate_jump_ reg_exps (Llvm.instr_begin dst) with
+  | [] -> (jmp, blocks)
+  | reg_exps ->
+      let mov =
+        Llair.Inst.move ~reg_exps:(Vector.of_list_rev reg_exps) ~loc
       in
-      (Option.cons instr_arg rev_args, pos)
-  | At_end blk -> fail "block_formals: %a" pp_llblock blk ()
-
-(** actual arguments passed by a jump to a block *)
-let jump_args : x -> Llvm.llvalue -> Llvm.llbasicblock -> Exp.t list =
- fun x jmp dst ->
-  let src = Llvm.instr_parent jmp in
-  let retn_arg, rev_args, _ =
-    rev_map_phis dst ~f:(fun phi ->
-        Option.value_exn
-          (List.find_map (Llvm.incoming phi) ~f:(fun (arg, pred) ->
-               if Poly.equal pred src then Some (xlate_value x arg)
-               else None )) )
-  in
-  let retn_arg =
-    Option.first_some retn_arg
-      (Option.map (unique_used_invoke_pred dst) ~f:(fun invoke ->
-           Exp.var (xlate_name invoke) ))
-  in
-  Option.cons retn_arg rev_args
+      let lbl = find_name instr ^ ".jmp" in
+      let blk =
+        Llair.Block.mk ~lbl
+          ~cmnd:(Vector.of_array [|mov|])
+          ~term:(Llair.Term.goto ~dst:jmp ~loc)
+      in
+      (Llair.Jump.mk lbl, blk :: blocks)
 
 (** An LLVM instruction is translated to a sequence of LLAIR instructions
     and a terminator, plus some additional blocks to which it may refer
@@ -1025,24 +924,21 @@ let xlate_instr :
               List.rev_init num_args ~f:(fun i ->
                   xlate_value x (Llvm.operand instr i) )
             in
-            let return = Llair.Jump.mk lbl [] in
-            Llair.Term.call ~func ~typ ~args ~loc ~return ~throw:None
-              ~ignore_result:false
+            let areturn = xlate_name_opt instr in
+            let return = Llair.Jump.mk lbl in
+            Llair.Term.call ~func ~typ ~args ~areturn ~return ~throw:None
+              ~ignore_result:false ~loc
           in
-          let params = Option.to_list (xlate_name_opt instr) in
           continue (fun (insts, term) ->
               let cmnd = Vector.of_list insts in
-              ([], call, [Llair.Block.mk ~lbl ~params ~cmnd ~term]) ) )
+              ([], call, [Llair.Block.mk ~lbl ~cmnd ~term]) ) )
   | Invoke -> (
-      let reg = xlate_name_opt instr in
       let llfunc = Llvm.operand instr (Llvm.num_operands instr - 3) in
       let lltyp = Llvm.type_of llfunc in
       assert (Poly.(Llvm.classify_type lltyp = Pointer)) ;
       let fname = Llvm.value_name llfunc in
       let return_blk = Llvm.get_normal_dest instr in
-      let return_dst = label_of_block return_blk in
       let unwind_blk = Llvm.get_unwind_dest instr in
-      let unwind_dst = label_of_block unwind_blk in
       let num_args =
         if not (Llvm.is_var_arg (Llvm.element_type lltyp)) then
           Llvm.num_arg_operands instr
@@ -1058,15 +954,15 @@ let xlate_instr :
         List.rev_init num_args ~f:(fun i ->
             xlate_value x (Llvm.operand instr i) )
       in
+      let areturn = xlate_name_opt instr in
       (* intrinsics *)
       match String.split fname ~on:'.' with
       | _ when Option.is_some (xlate_intrinsic_exp fname) ->
-          let arg = Option.to_list (Option.map ~f:Exp.var reg) in
-          let dst = Llair.Jump.mk return_dst arg in
-          emit_term (Llair.Term.goto ~dst ~loc)
+          let dst, blocks = xlate_jump x instr return_blk loc [] in
+          emit_term (Llair.Term.goto ~dst ~loc) ~blocks
       | ["__llair_throw"] ->
-          let dst = Llair.Jump.mk unwind_dst args in
-          emit_term (Llair.Term.goto ~dst ~loc)
+          let dst, blocks = xlate_jump x instr unwind_blk loc [] in
+          emit_term (Llair.Term.goto ~dst ~loc) ~blocks
       | ["abort"] ->
           emit_term ~prefix:[Llair.Inst.abort ~loc] Llair.Term.unreachable
       | ["_Znwm" (* operator new(size_t num) *)]
@@ -1077,11 +973,11 @@ let xlate_instr :
           let num = xlate_value x (Llvm.operand instr 0) in
           let llt = Llvm.type_of instr in
           let len = Exp.integer (Z.of_int (size_of x llt)) Typ.siz in
-          let args = jump_args x instr return_blk in
-          let dst = Llair.Jump.mk return_dst args in
+          let dst, blocks = xlate_jump x instr return_blk loc [] in
           emit_term
             ~prefix:[Llair.Inst.alloc ~reg ~num ~len ~loc]
             (Llair.Term.goto ~dst ~loc)
+            ~blocks
       (* unimplemented *)
       | "llvm" :: "experimental" :: "gc" :: "statepoint" :: _ ->
           todo "statepoints:@ %a" pp_llvalue instr ()
@@ -1089,37 +985,18 @@ let xlate_instr :
       | _ ->
           let func = xlate_func_name x llfunc in
           let typ = xlate_type x (Llvm.type_of llfunc) in
+          let return, blocks = xlate_jump x instr return_blk loc [] in
+          let throw, blocks = xlate_jump x instr unwind_blk loc blocks in
+          let throw = Some throw in
           let ignore_result =
             match typ with
             | Pointer {elt= Function {return= Some _}} ->
-                not (return_formal_is_used instr)
+                Option.is_none (Llvm.use_begin instr)
             | _ -> false
           in
-          let return, blocks =
-            let args = trampoline_args x instr return_blk in
-            if not (need_return_trampoline instr return_blk) then
-              (Llair.Jump.mk return_dst args, [])
-            else
-              let lbl = name ^ ".ret" in
-              let block =
-                let params = [xlate_name instr] in
-                let cmnd = Vector.empty in
-                let term =
-                  let dst = Llair.Jump.mk return_dst args in
-                  Llair.Term.goto ~dst ~loc
-                in
-                Llair.Block.mk ~lbl ~params ~cmnd ~term
-              in
-              (Llair.Jump.mk lbl [], [block])
-          in
-          let throw =
-            let dst = unwind_dst in
-            let args = trampoline_args x instr unwind_blk in
-            Some (Llair.Jump.mk dst args)
-          in
           emit_term
-            (Llair.Term.call ~func ~typ ~args ~loc ~return ~throw
-               ~ignore_result)
+            (Llair.Term.call ~func ~typ ~args ~areturn ~return ~throw
+               ~ignore_result ~loc)
             ~blocks )
   | Ret ->
       let exp =
@@ -1130,61 +1007,53 @@ let xlate_instr :
   | Br -> (
     match Option.value_exn (Llvm.get_branch instr) with
     | `Unconditional blk ->
-        let args = jump_args x instr blk in
-        let dst = Llair.Jump.mk (label_of_block blk) args in
-        emit_term (Llair.Term.goto ~dst ~loc)
+        let dst, blocks = xlate_jump x instr blk loc [] in
+        emit_term (Llair.Term.goto ~dst ~loc) ~blocks
     | `Conditional (cnd, thn, els) ->
         let key = xlate_value x cnd in
-        let thn_lbl = label_of_block thn in
-        let thn_args = jump_args x instr thn in
-        let thn = Llair.Jump.mk thn_lbl thn_args in
-        let els_lbl = label_of_block els in
-        let els_args = jump_args x instr els in
-        let els = Llair.Jump.mk els_lbl els_args in
-        emit_term (Llair.Term.branch ~key ~nzero:thn ~zero:els ~loc) )
+        let thn, blocks = xlate_jump x instr thn loc [] in
+        let els, blocks = xlate_jump x instr els loc blocks in
+        emit_term (Llair.Term.branch ~key ~nzero:thn ~zero:els ~loc) ~blocks
+    )
   | Switch ->
       let key = xlate_value x (Llvm.operand instr 0) in
-      let cases =
+      let cases, blocks =
         let num_cases = (Llvm.num_operands instr / 2) - 1 in
-        let rec xlate_cases i =
+        let rec xlate_cases i blocks =
           if i <= num_cases then
             let idx = Llvm.operand instr (2 * i) in
             let blk =
               Llvm.block_of_value (Llvm.operand instr ((2 * i) + 1))
             in
             let num = xlate_value x idx in
-            let dst = label_of_block blk in
-            let args = jump_args x instr blk in
-            let rest = xlate_cases (i + 1) in
-            (num, Llair.Jump.mk dst args) :: rest
-          else []
+            let jmp, blocks = xlate_jump x instr blk loc blocks in
+            let rest, blocks = xlate_cases (i + 1) blocks in
+            ((num, jmp) :: rest, blocks)
+          else ([], blocks)
         in
-        xlate_cases 1
+        xlate_cases 1 []
       in
       let tbl = Vector.of_list cases in
       let blk = Llvm.block_of_value (Llvm.operand instr 1) in
-      let dst = label_of_block blk in
-      let args = jump_args x instr blk in
-      let els = Llair.Jump.mk dst args in
-      emit_term (Llair.Term.switch ~key ~tbl ~els ~loc)
+      let els, blocks = xlate_jump x instr blk loc blocks in
+      emit_term (Llair.Term.switch ~key ~tbl ~els ~loc) ~blocks
   | IndirectBr ->
       let ptr = xlate_value x (Llvm.operand instr 0) in
       let num_dests = Llvm.num_operands instr - 1 in
-      let lldests =
-        let rec dests i =
+      let lldests, blocks =
+        let rec dests i blocks =
           if i <= num_dests then
             let v = Llvm.operand instr i in
             let blk = Llvm.block_of_value v in
-            let dst = label_of_block blk in
-            let args = jump_args x instr blk in
-            let rest = dests (i + 1) in
-            Llair.Jump.mk dst args :: rest
-          else []
+            let jmp, blocks = xlate_jump x instr blk loc blocks in
+            let rest, blocks = dests (i + 1) blocks in
+            (jmp :: rest, blocks)
+          else ([], blocks)
         in
-        dests 1
+        dests 1 []
       in
       let tbl = Vector.of_list lldests in
-      emit_term (Llair.Term.iswitch ~ptr ~tbl ~loc)
+      emit_term (Llair.Term.iswitch ~ptr ~tbl ~loc) ~blocks
   | LandingPad ->
       (* Translate the landingpad clauses to code to load the type_info from
          the thrown exception, and test the type_info against the clauses,
@@ -1192,7 +1061,7 @@ let xlate_instr :
          passing a value for the selector which the handler code tests to
          e.g. either cleanup or rethrow. *)
       let i32, tip, cxa_exception = landingpad_typs x instr in
-      let exc = Exp.var (landingpad_arg instr) in
+      let exc = Exp.var (Var.program (find_name instr ^ ".exc")) in
       let ti = Var.program (name ^ ".ti") in
       (* std::type_info* ti = ((__cxa_exception* )exc - 1)->exceptionType *)
       let load_ti =
@@ -1213,33 +1082,44 @@ let xlate_instr :
       let typeid = xlate_llvm_eh_typeid_for x tip ti in
       let lbl = name ^ ".unwind" in
       let param = xlate_name instr in
-      let params = [param] in
-      let jump_unwind sel =
-        let dst = lbl in
-        let args = [Exp.record [exc; sel]] in
-        Llair.Jump.mk dst args
+      let jump_unwind i sel rev_blocks =
+        let arg = Exp.record [exc; sel] in
+        let mov =
+          Llair.Inst.move ~reg_exps:(Vector.of_array [|(param, arg)|]) ~loc
+        in
+        let lbl = lbl ^ "." ^ Int.to_string i in
+        let blk =
+          Llair.Block.mk ~lbl
+            ~cmnd:(Vector.of_array [|mov|])
+            ~term:(Llair.Term.goto ~dst:(Llair.Jump.mk lbl) ~loc)
+        in
+        (Llair.Jump.mk lbl, blk :: rev_blocks)
       in
-      let goto_unwind sel =
-        let dst = jump_unwind sel in
-        Llair.Term.goto ~dst ~loc
+      let goto_unwind i sel blocks =
+        let dst, blocks = jump_unwind i sel blocks in
+        (Llair.Term.goto ~dst ~loc, blocks)
       in
       let term_unwind, rev_blocks =
         if Llvm.is_cleanup instr then
-          (goto_unwind (Exp.integer Z.zero i32), [])
+          goto_unwind 0 (Exp.integer Z.zero i32) []
         else
           let num_clauses = Llvm.num_operands instr in
           let lbl i = name ^ "." ^ Int.to_string i in
-          let jump i = Llair.Jump.mk (lbl i) [] in
+          let jump i = Llair.Jump.mk (lbl i) in
           let block i term =
-            Llair.Block.mk ~lbl:(lbl i) ~params:[] ~cmnd:Vector.empty ~term
+            Llair.Block.mk ~lbl:(lbl i) ~cmnd:Vector.empty ~term
           in
-          let match_filter =
-            jump_unwind (Exp.sub i32 (Exp.integer Z.zero i32) typeid)
+          let match_filter i rev_blocks =
+            jump_unwind i
+              (Exp.sub i32 (Exp.integer Z.zero i32) typeid)
+              rev_blocks
           in
-          let xlate_clause i =
+          let xlate_clause i rev_blocks =
             let clause = Llvm.operand instr i in
             let num_tis = Llvm.num_operands clause in
-            if num_tis = 0 then Llair.Term.goto ~dst:match_filter ~loc
+            if num_tis = 0 then
+              let dst, rev_blocks = match_filter i rev_blocks in
+              (Llair.Term.goto ~dst ~loc, rev_blocks)
             else
               match Llvm.classify_type (Llvm.type_of clause) with
               | Array (* filter *) -> (
@@ -1252,30 +1132,32 @@ let xlate_instr :
                       else Exp.dq tiI ti
                     in
                     let key = xlate_filter 0 in
-                    Llair.Term.branch ~loc ~key ~nzero:match_filter
-                      ~zero:(jump (i + 1))
+                    let nzero, rev_blocks = match_filter i rev_blocks in
+                    ( Llair.Term.branch ~loc ~key ~nzero ~zero:(jump (i + 1))
+                    , rev_blocks )
                 | _ -> fail "xlate_instr: %a" pp_llvalue instr () )
               | _ (* catch *) ->
                   let clause = xlate_value x clause in
                   let key =
                     Exp.or_ (Exp.eq clause Exp.null) (Exp.eq clause ti)
                   in
-                  Llair.Term.branch ~loc ~key ~nzero:(jump_unwind typeid)
-                    ~zero:(jump (i + 1))
+                  let nzero, rev_blocks = jump_unwind i typeid rev_blocks in
+                  ( Llair.Term.branch ~loc ~key ~nzero ~zero:(jump (i + 1))
+                  , rev_blocks )
           in
           let rec rev_blocks i z =
             if i < num_clauses then
-              rev_blocks (i + 1) (block i (xlate_clause i) :: z)
+              let term, z = xlate_clause i z in
+              rev_blocks (i + 1) (block i term :: z)
             else block i Llair.Term.unreachable :: z
           in
-          (xlate_clause 0, rev_blocks 1 [])
+          xlate_clause 0 (rev_blocks 1 [])
       in
       continue (fun (insts, term) ->
           ( [load_ti]
           , term_unwind
           , List.rev_append rev_blocks
-              [ Llair.Block.mk ~lbl ~params ~cmnd:(Vector.of_list insts)
-                  ~term ] ) )
+              [Llair.Block.mk ~lbl ~cmnd:(Vector.of_list insts) ~term] ) )
   | Resume ->
       let rcd = xlate_value x (Llvm.operand instr 0) in
       let exc = Exp.select ~rcd ~idx:(Exp.integer Z.zero Typ.siz) in
@@ -1298,6 +1180,18 @@ let xlate_instr :
       fail "xlate_instr: %a" pp_llvalue instr ()
   | PHI | Invalid | Invalid2 | UserOp1 | UserOp2 -> assert false
 
+let skip_phis : Llvm.llbasicblock -> _ Llvm.llpos =
+ fun blk ->
+  let rec skip_phis_ (pos : _ Llvm.llpos) =
+    match pos with
+    | Before instr -> (
+      match Llvm.instr_opcode instr with
+      | PHI -> skip_phis_ (Llvm.instr_succ instr)
+      | _ -> pos )
+    | _ -> pos
+  in
+  skip_phis_ (Llvm.instr_begin blk)
+
 let rec xlate_instrs : pop_thunk -> x -> _ Llvm.llpos -> code =
  fun pop x -> function
   | Before instrI ->
@@ -1313,9 +1207,9 @@ let xlate_block : pop_thunk -> x -> Llvm.llbasicblock -> Llair.block list =
   [%Trace.call fun {pf} -> pf "%a" pp_llblock blk]
   ;
   let lbl = label_of_block blk in
-  let params, pos = block_formals blk in
+  let pos = skip_phis blk in
   let insts, term, blocks = xlate_instrs pop x pos in
-  Llair.Block.mk ~lbl ~params ~cmnd:(Vector.of_list insts) ~term :: blocks
+  Llair.Block.mk ~lbl ~cmnd:(Vector.of_list insts) ~term :: blocks
   |>
   [%Trace.retn fun {pf} blocks -> pf "%s" (List.hd_exn blocks).Llair.lbl]
 
@@ -1341,8 +1235,7 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func =
       in
       let entry =
         let {Llair.lbl; cmnd; term} = entry_block in
-        assert (List.is_empty entry_block.params) ;
-        Llair.Block.mk ~lbl ~params ~cmnd ~term
+        Llair.Block.mk ~lbl ~cmnd ~term
       in
       let cfg =
         let rec trav_blocks rev_cfg prev =
@@ -1355,7 +1248,7 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func =
         in
         trav_blocks (List.rev entry_blocks) entry_blk
       in
-      Llair.Func.mk ~name ~entry ~cfg
+      Llair.Func.mk ~name ~params ~entry ~cfg
   | At_end _ ->
       report_undefined llf name ;
       Llair.Func.mk_undefined ~name ~params )
diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml
index a0aadf903..146cb06b2 100644
--- a/sledge/src/llair/llair.ml
+++ b/sledge/src/llair/llair.ml
@@ -5,7 +5,9 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-(** Translation units *)
+(** LLAIR (Low-Level Analysis Internal Representation) *)
+
+[@@@warning "+9"]
 
 type inst =
   | Move of {reg_exps: (Var.t * Exp.t) vector; loc: Loc.t}
@@ -23,29 +25,29 @@ type inst =
 type cmnd = inst vector [@@deriving sexp]
 type label = string [@@deriving sexp]
 
-type 'a control_transfer =
-  {mutable dst: 'a; args: Exp.t list; mutable retreating: bool}
-[@@deriving compare, equal, sexp_of]
+type jump = {mutable dst: block; mutable retreating: bool}
 
-type jump = block control_transfer
+and 'a call =
+  { callee: 'a
+  ; typ: Typ.t
+  ; args: Exp.t list
+  ; areturn: Var.t option
+  ; return: jump
+  ; throw: jump option
+  ; ignore_result: bool
+  ; mutable recursive: bool
+  ; loc: Loc.t }
 
 and term =
   | Switch of {key: Exp.t; tbl: (Exp.t * jump) vector; els: jump; loc: Loc.t}
   | Iswitch of {ptr: Exp.t; tbl: jump vector; loc: Loc.t}
-  | Call of
-      { call: Exp.t control_transfer
-      ; typ: Typ.t
-      ; return: jump
-      ; throw: jump option
-      ; ignore_result: bool
-      ; loc: Loc.t }
+  | Call of Exp.t call
   | Return of {exp: Exp.t option; loc: Loc.t}
   | Throw of {exc: Exp.t; loc: Loc.t}
   | Unreachable
 
 and block =
   { lbl: label
-  ; params: Var.t list
   ; cmnd: cmnd
   ; term: term
   ; mutable parent: func
@@ -53,15 +55,15 @@ and block =
 
 and cfg = block vector
 
-(* [entry] is not part of [cfg] since it is special in several ways: its
-   params are the func params, and it cannot be jumped to, only called. *)
+(* [entry] is not part of [cfg] since it cannot be jumped to, only called. *)
 and func =
   { name: Global.t
+  ; params: Var.t list
+  ; freturn: Var.t option
+  ; fthrow: Var.t
   ; locals: Var.Set.t
   ; entry: block
-  ; cfg: cfg
-  ; freturn: Var.t option
-  ; fthrow: Var.t }
+  ; cfg: cfg }
 
 let sexp_cons (hd : Sexp.t) (tl : Sexp.t) =
   match tl with
@@ -70,8 +72,8 @@ let sexp_cons (hd : Sexp.t) (tl : Sexp.t) =
 
 let sexp_ctor label args = sexp_cons (Sexp.Atom label) args
 
-let sexp_of_jump {dst; args; retreating} =
-  [%sexp {dst: label = dst.lbl; args: Exp.t list; retreating: bool}]
+let sexp_of_jump {dst; retreating} =
+  [%sexp {dst: label = dst.lbl; retreating: bool}]
 
 let sexp_of_term = function
   | Switch {key; tbl; els; loc} ->
@@ -80,24 +82,35 @@ let sexp_of_term = function
           {key: Exp.t; tbl: (Exp.t * jump) vector; els: jump; loc: Loc.t}]
   | Iswitch {ptr; tbl; loc} ->
       sexp_ctor "Iswitch" [%sexp {ptr: Exp.t; tbl: jump vector; loc: Loc.t}]
-  | Call {call; typ; return; throw; ignore_result; loc} ->
+  | Call
+      { callee
+      ; typ
+      ; args
+      ; areturn
+      ; return
+      ; throw
+      ; ignore_result
+      ; recursive
+      ; loc } ->
       sexp_ctor "Call"
         [%sexp
-          { call: Exp.t control_transfer
+          { callee: Exp.t
           ; typ: Typ.t
+          ; args: Exp.t list
+          ; areturn: Var.t option
           ; return: jump
           ; throw: jump option
           ; ignore_result: bool
+          ; recursive: bool
           ; loc: Loc.t }]
   | Return {exp; loc} ->
       sexp_ctor "Return" [%sexp {exp: Exp.t option; loc: Loc.t}]
   | Throw {exc; loc} -> sexp_ctor "Throw" [%sexp {exc: Exp.t; loc: Loc.t}]
   | Unreachable -> Sexp.Atom "Unreachable"
 
-let sexp_of_block {lbl; params; cmnd; term; parent; sort_index} =
+let sexp_of_block {lbl; cmnd; term; parent; sort_index} =
   [%sexp
     { lbl: label
-    ; params: Var.t list
     ; cmnd: cmnd
     ; term: term
     ; parent: Var.t = parent.name.var
@@ -105,8 +118,15 @@ let sexp_of_block {lbl; params; cmnd; term; parent; sort_index} =
 
 let sexp_of_cfg v = [%sexp_of: block vector] v
 
-let sexp_of_func {name; locals; entry; cfg} =
-  [%sexp {name: Global.t; locals: Var.Set.t; entry: block; cfg: cfg}]
+let sexp_of_func {name; params; freturn; fthrow; locals; entry; cfg} =
+  [%sexp
+    { name: Global.t
+    ; params: Var.t list
+    ; freturn: Var.t option
+    ; fthrow: Var.t
+    ; locals: Var.Set.t
+    ; entry: block
+    ; cfg: cfg }]
 
 (* blocks in a [t] are uniquely identified by [sort_index] *)
 let compare_block x y = Int.compare x.sort_index y.sort_index
@@ -125,7 +145,7 @@ let pp_inst fs inst =
       pf "@[<2>@[%a@]@ := @[%a@];@]\t%a" (Vector.pp ",@ " Var.pp) regs
         (Vector.pp ",@ " Exp.pp) exps Loc.pp loc
   | Load {reg; ptr; len; loc} ->
-      pf "@[<2>load %a@ %a@ %a;@]\t%a" Exp.pp len Var.pp reg Exp.pp ptr
+      pf "@[<2>%a@ := load %a@ %a;@]\t%a" Var.pp reg Exp.pp len Exp.pp ptr
         Loc.pp loc
   | Store {ptr; exp; len; loc} ->
       pf "@[<2>store %a@ %a@ %a;@]\t%a" Exp.pp len Exp.pp ptr Exp.pp exp
@@ -140,12 +160,13 @@ let pp_inst fs inst =
       pf "@[<2>memmov %a %a %a;@]\t%a" Exp.pp len Exp.pp dst Exp.pp src
         Loc.pp loc
   | Alloc {reg; num; len; loc} ->
-      pf "@[<2>alloc %a@ [%a x %a];@]\t%a" Var.pp reg Exp.pp num Exp.pp len
-        Loc.pp loc
+      pf "@[<2>%a@ := alloc [%a x %a];@]\t%a" Var.pp reg Exp.pp num Exp.pp
+        len Loc.pp loc
   | Free {ptr; loc} -> pf "@[<2>free %a;@]\t%a" Exp.pp ptr Loc.pp loc
   | Nondet {reg; msg; loc} ->
-      pf "@[<2>nondet %a\"%s\";@]\t%a" (Option.pp "%a " Var.pp) reg msg
-        Loc.pp loc
+      pf "@[<2>%anondet \"%s\";@]\t%a"
+        (Option.pp "%a := " Var.pp)
+        reg msg Loc.pp loc
   | Abort {loc} -> pf "@[<2>abort;@]\t%a" Loc.pp loc
 
 let pp_args pp_arg fs args =
@@ -153,10 +174,10 @@ let pp_args pp_arg fs args =
 
 let pp_param fs var = Var.pp fs var
 
-let pp_jump fs {dst= {lbl}; args; retreating} =
-  Format.fprintf fs "@[<2>%s%%%s%a@]"
+let pp_jump fs {dst; retreating} =
+  Format.fprintf fs "@[<2>%s%%%s@]"
     (if retreating then "↑" else "")
-    lbl (pp_args Exp.pp) args
+    dst.lbl
 
 let pp_term fs term =
   let pf pp = Format.fprintf fs pp in
@@ -175,13 +196,15 @@ let pp_term fs term =
           tbl pp_goto els Loc.pp loc )
   | Iswitch {ptr; tbl; loc} ->
       pf "@[<2>iswitch %a@ @[<hv>%a@]@]\t%a" Exp.pp ptr
-        (Vector.pp "@ " (fun fs ({dst= {lbl}; _} as jmp) ->
-             Format.fprintf fs "%s: %a" lbl pp_goto jmp ))
+        (Vector.pp "@ " (fun fs jmp ->
+             Format.fprintf fs "%s: %a" jmp.dst.lbl pp_goto jmp ))
         tbl Loc.pp loc
-  | Call {call= {dst; args; retreating}; return; throw; loc} ->
-      pf "@[<2>@[<7>call @[<2>%s%a%a@]@]@ @[returnto %a%a;@]@]\t%a"
-        (if retreating then "↑" else "")
-        Exp.pp dst (pp_args Exp.pp) args pp_jump return
+  | Call {callee; args; areturn; return; throw; recursive; loc; _} ->
+      pf "@[<2>@[<7>%acall @[<2>%s%a%a@]@]@ @[returnto %a%a;@]@]\t%a"
+        (Option.pp "%a := " Var.pp)
+        areturn
+        (if recursive then "↑" else "")
+        Exp.pp callee (pp_args Exp.pp) args pp_jump return
         (Option.pp "@ throwto %a" pp_jump)
         throw Loc.pp loc
   | Return {exp; loc} ->
@@ -191,9 +214,9 @@ let pp_term fs term =
 
 let pp_cmnd = Vector.pp "@ " pp_inst
 
-let pp_block fs {lbl; params; cmnd; term; sort_index} =
-  Format.fprintf fs "@[<v 2>@[<4>%s%a@]: #%i@ @[<v>%a%t%a@]@]" lbl
-    (pp_args pp_param) params sort_index pp_cmnd cmnd
+let pp_block fs {lbl; cmnd; term; parent= _; sort_index} =
+  Format.fprintf fs "@[<v 2>%s: #%i@ @[<v>%a%t%a@]@]" lbl sort_index pp_cmnd
+    cmnd
     (fun fs -> if Vector.is_empty cmnd then () else Format.fprintf fs "@ ")
     pp_term term
 
@@ -201,7 +224,6 @@ let pp_block fs {lbl; params; cmnd; term; sort_index} =
 
 let rec dummy_block =
   { lbl= "dummy"
-  ; params= []
   ; cmnd= Vector.empty
   ; term= Unreachable
   ; parent= dummy_func
@@ -211,11 +233,12 @@ and dummy_func =
   let dummy_var = Var.program "dummy" in
   let dummy_ptr_typ = Typ.pointer ~elt:(Typ.opaque ~name:"dummy") in
   { name= Global.mk dummy_var dummy_ptr_typ Loc.none
+  ; params= []
+  ; freturn= None
+  ; fthrow= dummy_var
   ; locals= Var.Set.empty
   ; entry= dummy_block
-  ; cfg= Vector.empty
-  ; freturn= None
-  ; fthrow= dummy_var }
+  ; cfg= Vector.empty }
 
 (** Instructions *)
 
@@ -235,25 +258,26 @@ module Inst = struct
   let abort ~loc = Abort {loc}
 
   let loc = function
-    | Move {loc}
-     |Load {loc}
-     |Store {loc}
-     |Memset {loc}
-     |Memcpy {loc}
-     |Memmov {loc}
-     |Alloc {loc}
-     |Free {loc}
-     |Nondet {loc}
-     |Abort {loc} ->
+    | Move {loc; _}
+     |Load {loc; _}
+     |Store {loc; _}
+     |Memset {loc; _}
+     |Memcpy {loc; _}
+     |Memmov {loc; _}
+     |Alloc {loc; _}
+     |Free {loc; _}
+     |Nondet {loc; _}
+     |Abort {loc; _} ->
         loc
 
   let union_locals inst vs =
     match inst with
-    | Move {reg_exps} ->
+    | Move {reg_exps; _} ->
         Vector.fold ~f:(fun vs (reg, _) -> Set.add vs reg) ~init:vs reg_exps
-    | Load {reg} | Alloc {reg} | Nondet {reg= Some reg} -> Set.add vs reg
+    | Load {reg; _} | Alloc {reg; _} | Nondet {reg= Some reg; _} ->
+        Set.add vs reg
     | Store _ | Memcpy _ | Memmov _ | Memset _ | Free _
-     |Nondet {reg= None}
+     |Nondet {reg= None; _}
      |Abort _ ->
         vs
 
@@ -265,26 +289,10 @@ end
 module Jump = struct
   type t = jump [@@deriving sexp_of]
 
-  let compare = compare_control_transfer compare_block
-  let equal = equal_control_transfer equal_block
+  let compare x y = compare_block x.dst y.dst
+  let equal x y = equal_block x.dst y.dst
   let pp = pp_jump
-
-  let invariant ?(accept_return = false) jmp =
-    Invariant.invariant [%here] (jmp, accept_return) [%sexp_of: t * bool]
-    @@ fun () ->
-    let {dst= {params; parent}; args} = jmp in
-    if parent == dummy_func then
-      (* jmp not yet backpatched by Func.mk *)
-      assert true
-    else
-      assert (
-        List.length params = List.length args + Bool.to_int accept_return )
-
-  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}
+  let mk lbl = {dst= {dummy_block with lbl}; retreating= false}
 end
 
 (** Basic-Block Terminators *)
@@ -298,19 +306,14 @@ module Term = struct
     Invariant.invariant [%here] term [%sexp_of: t]
     @@ fun () ->
     match term with
-    | Switch {tbl; els} ->
-        Vector.iter tbl ~f:(fun (_, jmp) -> Jump.invariant jmp) ;
-        Jump.invariant els
-    | Iswitch {tbl} -> Vector.iter tbl ~f:Jump.invariant
-    | Call {call= {args= actls}; typ; return; throw; ignore_result} -> (
+    | Switch _ | Iswitch _ -> assert true
+    | Call {typ; args= actls; areturn; _} -> (
       match typ with
-      | Pointer {elt= Function {args= frmls; return= retn_typ}} ->
+      | Pointer {elt= Function {args= frmls; return= retn_typ; _}} ->
           assert (Vector.length frmls = List.length actls) ;
-          Jump.invariant return
-            ~accept_return:(Option.is_some retn_typ && not ignore_result) ;
-          Option.iter throw ~f:(Jump.invariant ~accept_return:true)
+          assert (Option.is_some retn_typ || Option.is_none areturn)
       | _ -> assert false )
-    | Return {exp} -> (
+    | Return {exp; _} -> (
       match parent with
       | Some parent ->
           assert (Bool.(Option.is_some exp = Option.is_some parent.freturn))
@@ -331,19 +334,36 @@ module Term = struct
 
   let iswitch ~ptr ~tbl ~loc = Iswitch {ptr; tbl; loc} |> check invariant
 
-  let call ~func ~typ ~args ~return ~throw ~ignore_result ~loc =
-    let call = {dst= func; args; retreating= false} in
-    Call {call; typ; return; throw; ignore_result; loc} |> check invariant
+  let call ~func ~typ ~args ~areturn ~return ~throw ~ignore_result ~loc =
+    Call
+      { callee= func
+      ; typ
+      ; args
+      ; areturn
+      ; return
+      ; throw
+      ; ignore_result
+      ; recursive= false
+      ; loc }
+    |> check invariant
 
   let return ~exp ~loc = Return {exp; loc} |> check invariant
   let throw ~exc ~loc = Throw {exc; loc} |> check invariant
   let unreachable = Unreachable |> check invariant
 
   let loc = function
-    | Switch {loc} | Iswitch {loc} | Call {loc} | Return {loc} | Throw {loc}
-      ->
+    | Switch {loc; _}
+     |Iswitch {loc; _}
+     |Call {loc; _}
+     |Return {loc; _}
+     |Throw {loc; _} ->
         loc
     | Unreachable -> Loc.none
+
+  let union_locals term vs =
+    match term with
+    | Call {areturn; _} -> Set.add_option areturn vs
+    | _ -> vs
 end
 
 (** Basic-Blocks *)
@@ -355,19 +375,12 @@ module Block = struct
 
   let pp = pp_block
 
-  let invariant blk =
-    Invariant.invariant [%here] blk [%sexp_of: t]
-    @@ fun () ->
-    assert (not (List.contains_dup blk.params ~compare:Var.compare))
-
-  let mk ~lbl ~params ~cmnd ~term =
+  let mk ~lbl ~cmnd ~term =
     { lbl
-    ; params
     ; cmnd
     ; term
     ; parent= dummy_block.parent
     ; sort_index= dummy_block.sort_index }
-    |> check invariant
 end
 
 (** Functions *)
@@ -376,16 +389,25 @@ module Func = struct
   type t = func [@@deriving sexp_of]
 
   let is_undefined = function
-    | {entry= {cmnd; term= Unreachable}} -> Vector.is_empty cmnd
+    | {entry= {cmnd; term= Unreachable; _}; _} -> Vector.is_empty cmnd
     | _ -> false
 
-  let pp fs ({name; entry= {params; cmnd; term; sort_index}; cfg} as func) =
+  let pp fs
+      ( { name
+        ; params
+        ; freturn
+        ; fthrow= _
+        ; locals= _
+        ; entry= {cmnd; term; sort_index; _}
+        ; cfg } as func ) =
     let pp_if cnd str fs = if cnd then Format.fprintf fs str in
-    Format.fprintf fs "@[<v>@[<v>%a@[<2>%a%a@]%t@]" (Option.pp "%a " Typ.pp)
+    Format.fprintf fs "@[<v>@[<v>%a%a@[<2>%a%a@]%t@]"
+      (Option.pp "%a " Typ.pp)
       ( match name.typ with
-      | Pointer {elt= Function {return}} -> return
+      | Pointer {elt= Function {return; _}} -> return
       | _ -> None )
-      Global.pp name (pp_args pp_param) params
+      (Option.pp " %a := " Var.pp)
+      freturn Global.pp name (pp_args pp_param) params
       (fun fs ->
         if is_undefined func then Format.fprintf fs " #%i@]" sort_index
         else
@@ -395,57 +417,51 @@ module Func = struct
             (Vector.pp "@\n@\n  " Block.pp)
             cfg )
 
-  let fold_term {entry= {term}; cfg} ~init ~f =
-    Vector.fold cfg ~init:(f init term) ~f:(fun a {term} -> f a term)
+  let fold_term {entry; cfg; _} ~init ~f =
+    Vector.fold cfg ~init:(f init entry.term) ~f:(fun a blk -> f a blk.term)
 
-  let iter_term {entry= {term}; cfg} ~f =
-    f term ;
-    Vector.iter cfg ~f:(fun {term} -> f term)
+  let iter_term {entry; cfg; _} ~f =
+    f entry.term ;
+    Vector.iter cfg ~f:(fun blk -> f blk.term)
 
   let invariant func =
     Invariant.invariant [%here] func [%sexp_of: t]
     @@ fun () ->
     assert (func == func.entry.parent) ;
-    let {name= {typ}; entry; cfg} = func in
+    let {name= {typ; _}; cfg; _} = func in
     match typ with
-    | Pointer {elt= Function {return}} ->
+    | Pointer {elt= Function {return; _}} ->
         assert (
           not
             (Vector.contains_dup cfg ~compare:(fun b1 b2 ->
                  String.compare b1.lbl b2.lbl )) ) ;
-        assert (
-          not
-            (List.contains_dup
-               (List.concat_map (entry :: Vector.to_list cfg) ~f:(fun blk ->
-                    blk.params ))
-               ~compare:Var.compare) ) ;
         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
 
-  let mk ~(name : Global.t) ~entry ~cfg =
+  let mk ~(name : Global.t) ~params ~entry ~cfg =
     let locals =
       let locals_cmnd locals cmnd =
         Vector.fold_right ~f:Inst.union_locals cmnd ~init:locals
       in
       let locals_block locals block =
-        Set.add_list block.params (locals_cmnd locals block.cmnd)
+        locals_cmnd (Term.union_locals block.term locals) block.cmnd
       in
-      let init = locals_cmnd Var.Set.empty entry.cmnd in
+      let init = locals_block Var.Set.empty entry in
       Vector.fold ~f:locals_block cfg ~init
     in
-    let wrt = Set.add_list entry.params locals in
+    let wrt = Set.add_list params locals in
     let freturn, wrt =
       match name.typ with
-      | Pointer {elt= Function {return= Some _}} ->
+      | Pointer {elt= Function {return= Some _; _}} ->
           let freturn, wrt = Var.fresh "freturn" ~wrt in
           (Some freturn, wrt)
       | _ -> (None, wrt)
     in
     let fthrow, _ = Var.fresh "fthrow" ~wrt in
-    let func = {name; locals; entry; cfg; freturn; fthrow} in
+    let func = {name; params; freturn; fthrow; locals; entry; cfg} in
     let resolve_parent_and_jumps block =
       block.parent <- func ;
       let lookup cfg lbl : block =
@@ -453,11 +469,11 @@ module Func = struct
       in
       let set_dst jmp = jmp.dst <- lookup cfg jmp.dst.lbl in
       match block.term with
-      | Switch {tbl; els} ->
+      | Switch {tbl; els; _} ->
           Vector.iter tbl ~f:(fun (_, jmp) -> set_dst jmp) ;
           set_dst els
-      | Iswitch {tbl} -> Vector.iter tbl ~f:set_dst
-      | Call {return; throw} ->
+      | Iswitch {tbl; _} -> Vector.iter tbl ~f:set_dst
+      | Call {return; throw; _} ->
           set_dst return ;
           Option.iter throw ~f:set_dst
       | Return _ | Throw _ | Unreachable -> ()
@@ -468,10 +484,10 @@ module Func = struct
 
   let mk_undefined ~name ~params =
     let entry =
-      Block.mk ~lbl:"" ~params ~cmnd:Vector.empty ~term:Term.unreachable
+      Block.mk ~lbl:"" ~cmnd:Vector.empty ~term:Term.unreachable
     in
     let cfg = Vector.empty in
-    mk ~name ~entry ~cfg
+    mk ~name ~entry ~params ~cfg
 end
 
 (** Derived meta-data *)
@@ -509,8 +525,8 @@ let set_derived_metadata functions =
         FuncQ.enqueue_back_exn roots func.name.var func ) ;
     Map.iter functions ~f:(fun func ->
         Func.fold_term func ~init:() ~f:(fun () -> function
-          | Call {call= {dst}} -> (
-            match Var.of_exp dst with
+          | Call {callee; _} -> (
+            match Var.of_exp callee with
             | Some callee ->
                 FuncQ.remove roots callee |> (ignore : [> ] -> unit)
             | None -> () )
@@ -528,18 +544,18 @@ let set_derived_metadata functions =
           else visit ancestors func jmp.dst
         in
         ( match src.term with
-        | Switch {tbl; els} ->
+        | Switch {tbl; els; _} ->
             Vector.iter tbl ~f:(fun (_, jmp) -> jump jmp) ;
             jump els
-        | Iswitch {tbl} -> Vector.iter tbl ~f:jump
-        | Call {call= {dst} as call; return; throw} ->
-            ( match Var.of_exp dst >>= Func.find functions with
+        | Iswitch {tbl; _} -> Vector.iter tbl ~f:jump
+        | Call ({callee; return; throw; _} as call) ->
+            ( match Var.of_exp callee >>= Func.find functions with
             | Some func ->
-                if Set.mem ancestors func.entry then call.retreating <- true
+                if Set.mem ancestors func.entry then call.recursive <- true
                 else visit ancestors func func.entry
             | None ->
                 (* conservatively assume all virtual calls are recursive *)
-                call.retreating <- true ) ;
+                call.recursive <- true ) ;
             jump return ; Option.iter ~f:jump throw
         | Return _ | Throw _ | Unreachable -> () ) ;
         BlockQ.enqueue_back_exn tips_to_roots src ()
@@ -555,7 +571,7 @@ let set_derived_metadata functions =
         index := !index - 1 )
   in
   let sort_cfgs functions =
-    Map.iter functions ~f:(fun {cfg} ->
+    Map.iter functions ~f:(fun {cfg; _} ->
         Array.sort
           ~compare:(fun x y -> Int.compare x.sort_index y.sort_index)
           (Vector.to_array cfg) )
diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli
index 715ec4543..1addff835 100644
--- a/sledge/src/llair/llair.mli
+++ b/sledge/src/llair/llair.mli
@@ -5,28 +5,8 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-(** Translation units
-
-    LLAIR (Low-Level Analysis Internal Representation) is an IR tailored for
-    static analysis using a low-level model of memory. Compared to a
-    compiler IR such as LLVM, an analyzer does not need to perform register
-    allocation, instruction selection, code generation, etc. or even much
-    code transformation, so the constraints on the IR are very different.
-
-    LLAIR is a "Functional SSA" form where control transfers pass arguments
-    instead of using ϕ-nodes. An analyzer will need good support for
-    parameter passing anyhow, and ϕ-nodes make it hard to express program
-    properties as predicates on states, since some execution history is
-    needed to evaluate ϕ instructions. An alternative view is that the scope
-    of variables [reg] assigned in instructions such as [Load] is the
-    successor block as well as all blocks the instruction dominates in the
-    control-flow graph. This language is first-order, and a term structure
-    for the code constituting the scope of variables is not needed, so SSA
-    rather than full CPS suffices.
-
-    Additionally, the focus on memory analysis leads to a design where the
-    arithmetic and logic operations are not "instructions" but instead are
-    complex expressions (see [Exp]) that refer to registers (see [Var]). *)
+(** LLAIR (Low-Level Analysis Internal Representation) is an IR tailored for
+    static analysis using a low-level model of memory. *)
 
 (** Instructions for memory manipulation or other non-control effects. *)
 type inst = private
@@ -61,15 +41,21 @@ type cmnd = inst vector
 (** A label is a name of a block. *)
 type label = string
 
-(** A jump with arguments. *)
-type 'a control_transfer =
-  { mutable dst: 'a
-  ; args: Exp.t list  (** Stack of arguments, first-arg-last *)
-  ; mutable retreating: bool
-        (** Holds if [dst] is an ancestor in a depth-first traversal. *) }
-
-(** A jump with arguments to a block. *)
-type jump = block control_transfer
+(** A jump to a block. *)
+type jump = {mutable dst: block; mutable retreating: bool}
+
+(** A call to a function. *)
+and 'a call =
+  { callee: 'a
+  ; typ: Typ.t  (** Type of the callee. *)
+  ; args: Exp.t list  (** Stack of arguments, first-arg-last. *)
+  ; areturn: Var.t option  (** Register to receive return value. *)
+  ; return: jump  (** Return destination. *)
+  ; throw: jump option  (** Handler destination. *)
+  ; ignore_result: bool  (** Drop return value when invoking return. *)
+  ; mutable recursive: bool
+        (** Holds unless [callee] is definitely not recursive. *)
+  ; loc: Loc.t }
 
 (** Block terminators for function call/return or other control transfers. *)
 and term = private
@@ -78,14 +64,8 @@ and term = private
           [case] which is equal to [key], if any, otherwise invoke [els]. *)
   | Iswitch of {ptr: Exp.t; tbl: jump vector; loc: Loc.t}
       (** Invoke the [jump] in [tbl] whose [dst] is equal to [ptr]. *)
-  | Call of
-      { call: Exp.t control_transfer  (** A [global] for non-virtual call. *)
-      ; typ: Typ.t  (** Type of the callee. *)
-      ; return: jump  (** Return destination or trampoline. *)
-      ; throw: jump option  (** Handler destination or trampoline. *)
-      ; ignore_result: bool  (** Drop return value when invoking return. *)
-      ; loc: Loc.t }
-      (** Call function [call.dst] with arguments [call.args]. *)
+  | Call of Exp.t call
+      (** Call function with arguments. A [global] for non-virtual call. *)
   | Return of {exp: Exp.t option; loc: Loc.t}
       (** Invoke [return] of the dynamically most recent [Call]. *)
   | Throw of {exc: Exp.t; loc: Loc.t}
@@ -97,7 +77,6 @@ and term = private
 (** A block is a destination of a jump with arguments, contains code. *)
 and block = private
   { lbl: label
-  ; params: Var.t list  (** Formal parameters, first-param-last stack *)
   ; cmnd: cmnd
   ; term: term
   ; mutable parent: func
@@ -111,11 +90,12 @@ and cfg
     parameters are the function parameters. *)
 and func = private
   { name: Global.t
+  ; params: Var.t list  (** Formal parameters, first-param-last stack *)
+  ; freturn: Var.t option
+  ; fthrow: Var.t
   ; locals: Var.Set.t  (** Local variables *)
   ; entry: block
-  ; cfg: cfg
-  ; freturn: Var.t option
-  ; fthrow: Var.t }
+  ; cfg: cfg }
 
 type functions
 
@@ -151,8 +131,7 @@ module Jump : sig
   type t = jump [@@deriving compare, equal, sexp_of]
 
   val pp : jump pp
-  val mk : string -> Exp.t list -> jump
-  val push_arg : Exp.t -> jump -> jump
+  val mk : string -> jump
 end
 
 module Term : sig
@@ -175,6 +154,7 @@ module Term : sig
        func:Exp.t
     -> typ:Typ.t
     -> args:Exp.t list
+    -> areturn:Var.t option
     -> return:jump
     -> throw:jump option
     -> ignore_result:bool
@@ -193,10 +173,7 @@ module Block : sig
   include Comparator.S with type t := t
 
   val pp : t pp
-
-  include Invariant.S with type t := t
-
-  val mk : lbl:label -> params:Var.t list -> cmnd:cmnd -> term:term -> block
+  val mk : lbl:label -> cmnd:cmnd -> term:term -> block
 end
 
 module Func : sig
@@ -206,7 +183,13 @@ module Func : sig
 
   include Invariant.S with type t := t
 
-  val mk : name:Global.t -> entry:block -> cfg:block vector -> func
+  val mk :
+       name:Global.t
+    -> params:Var.t list
+    -> entry:block
+    -> cfg:block vector
+    -> func
+
   val mk_undefined : name:Global.t -> params:Var.t list -> t
 
   val find : functions -> Var.t -> func option
diff --git a/sledge/src/report.ml b/sledge/src/report.ml
index 3a5ae8d28..8324f16e0 100644
--- a/sledge/src/report.ml
+++ b/sledge/src/report.ml
@@ -15,10 +15,10 @@ let unknown_call call =
       call
       (fun fs (call : Llair.Term.t) ->
         match call with
-        | Call {call= {dst}} -> (
-          match Var.of_exp dst with
+        | Call {callee} -> (
+          match Var.of_exp callee with
           | Some var -> Var.pp_demangled fs var
-          | None -> Exp.pp fs dst )
+          | None -> Exp.pp fs callee )
         | _ -> () )
       call Llair.Term.pp call]
 
diff --git a/sledge/src/symbheap/domain.ml b/sledge/src/symbheap/domain.ml
index a639b3841..dcd25398e 100644
--- a/sledge/src/symbheap/domain.ml
+++ b/sledge/src/symbheap/domain.ml
@@ -29,17 +29,21 @@ let exec_assume (entry, current) cnd =
   | Some current -> Some (entry, current)
   | None -> None
 
+let exec_kill (entry, current) reg =
+  (entry, State_domain.exec_kill current reg)
+
+let exec_move (entry, current) formal actual =
+  (entry, State_domain.exec_move current formal actual)
+
 let exec_inst (entry, current) inst =
   match State_domain.exec_inst current inst with
   | 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 ~skip_throw (entry, current) result intrinsic actuals =
+let exec_intrinsic ~skip_throw (entry, current) areturn intrinsic actuals =
   match
-    State_domain.exec_intrinsic ~skip_throw current result intrinsic actuals
+    State_domain.exec_intrinsic ~skip_throw current areturn intrinsic
+      actuals
   with
   | None -> None
   | Some (Ok current) -> Some (Ok (entry, current))
@@ -49,11 +53,8 @@ type from_call =
   {state_from_call: State_domain.from_call; caller_entry: State_domain.t}
 [@@deriving sexp_of]
 
-let jump actuals formals ?temps (entry, current) =
-  let current, _ = State_domain.jump actuals formals ?temps current in
-  (entry, current)
-
-let call ~summaries actuals formals locals globals_vec (entry, current) =
+let call ~summaries actuals areturn formals locals globals_vec
+    (entry, current) =
   let globals =
     Var.Set.of_vector
       (Vector.map globals_vec ~f:(fun (g : Global.t) -> g.var))
@@ -67,7 +68,8 @@ let call ~summaries actuals formals locals globals_vec (entry, current) =
        State_domain.pp current]
   ;
   let caller_current, state_from_call =
-    State_domain.call ~summaries actuals formals locals globals current
+    State_domain.call ~summaries actuals areturn formals locals globals
+      current
   in
   ((caller_current, caller_current), {state_from_call; caller_entry= entry}))
   |>
@@ -80,10 +82,10 @@ let post locals {caller_entry} (_, current) =
   |>
   [%Trace.retn fun {pf} -> pf "@,%a" pp]
 
-let retn formals {caller_entry; state_from_call} (_, current) =
+let retn formals freturn {caller_entry; state_from_call} (_, current) =
   [%Trace.call fun {pf} -> pf "@,%a" State_domain.pp current]
   ;
-  (caller_entry, State_domain.retn formals state_from_call current)
+  (caller_entry, State_domain.retn formals freturn 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 581d3e124..5fc8bd2ef 100644
--- a/sledge/src/symbheap/domain.mli
+++ b/sledge/src/symbheap/domain.mli
@@ -15,8 +15,9 @@ val init : Global.t vector -> t
 val join : t -> t -> t
 val is_false : t -> bool
 val exec_assume : t -> Exp.t -> t option
+val exec_kill : t -> Var.t -> t
+val exec_move : t -> Var.t -> Exp.t -> t
 val exec_inst : t -> Llair.inst -> (t, unit) result
-val exec_return : t -> Var.t -> Exp.t -> t
 
 val exec_intrinsic :
      skip_throw:bool
@@ -37,11 +38,11 @@ val create_summary :
   -> State_domain.function_summary * t
 
 val apply_summary : t -> State_domain.function_summary -> t option
-val jump : Exp.t list -> Var.t list -> ?temps:Var.Set.t -> t -> t
 
 val call :
      summaries:bool
   -> Exp.t list
+  -> Var.t option
   -> Var.t list
   -> Var.Set.t
   -> Global.t vector
@@ -49,7 +50,7 @@ val call :
   -> t * from_call
 
 val post : Var.Set.t -> from_call -> t -> t
-val retn : Var.t list -> from_call -> t -> t
+val retn : Var.t list -> Var.t option -> from_call -> t -> t
 val dnf : t -> t list
 
 val resolve_callee :
diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml
index a83cca4bf..3b33e3d46 100644
--- a/sledge/src/symbheap/exec.ml
+++ b/sledge/src/symbheap/exec.ml
@@ -52,7 +52,6 @@ let assume pre cnd =
   if Sh.is_false post then None else Some post
 
 let kill pre reg = Sh.exists (Set.add Var.Set.empty reg) pre
-let return pre formal exp = Sh.and_ (Exp.eq (Exp.var formal) exp) pre
 
 (* { emp }
  *   rs := es
@@ -670,10 +669,10 @@ let exec_spec pre {xs; foot; sub; ms; post} =
           Format.fprintf fs "%a := " Var.Set.pp ms )
       ms Sh.pp post ;
     assert (
-      let vs = Set.diff (Set.diff foot.Sh.us xs) pre.Sh.us in
+      let vs = Set.diff (Set.diff foot.us xs) pre.us in
       Set.is_empty vs || Trace.fail "unbound foot: {%a}" Var.Set.pp vs ) ;
     assert (
-      let vs = Set.diff (Set.diff post.Sh.us xs) pre.Sh.us in
+      let vs = Set.diff (Set.diff post.us xs) pre.us in
       Set.is_empty vs || Trace.fail "unbound post: {%a}" Var.Set.pp vs )]
   ;
   let foot = Sh.extend_us xs foot in
@@ -698,6 +697,10 @@ let rec exec_specs pre = function
       exec_specs pre specs >>| fun posts -> Sh.or_ post posts
   | [] -> Ok (Sh.false_ pre.us)
 
+let move pre reg exp =
+  exec_spec pre (move_spec pre.us (Vector.of_array [|(reg, exp)|]))
+  |> function Ok post -> post | _ -> assert false
+
 let inst : Sh.t -> Llair.inst -> (Sh.t, unit) result =
  fun pre inst ->
   [%Trace.info
@@ -727,18 +730,18 @@ let intrinsic ~skip_throw :
     -> Var.t
     -> Exp.t list
     -> (Sh.t, unit) result option =
- fun pre result intrinsic actuals ->
+ fun pre areturn intrinsic actuals ->
   [%Trace.info
     "@[<2>exec intrinsic@ @[%a%a(@[%a@])@] from@ @[{ %a@ }@]@]"
       (Option.pp "%a := " Var.pp)
-      result Var.pp intrinsic (List.pp ",@ " Exp.pp) (List.rev actuals)
+      areturn Var.pp intrinsic (List.pp ",@ " Exp.pp) (List.rev actuals)
       Sh.pp pre] ;
   let us = pre.us in
   let name =
     let n = Var.name intrinsic in
     match String.index n '.' with None -> n | Some i -> String.prefix n i
   in
-  match (result, name, actuals) with
+  match (areturn, name, actuals) with
   (*
    * cstdlib - memory management
    *)
diff --git a/sledge/src/symbheap/exec.mli b/sledge/src/symbheap/exec.mli
index 2bedae2a1..c379acc39 100644
--- a/sledge/src/symbheap/exec.mli
+++ b/sledge/src/symbheap/exec.mli
@@ -8,7 +8,8 @@
 (** Symbolic Execution *)
 
 val assume : Sh.t -> Exp.t -> Sh.t option
-val return : Sh.t -> Var.t -> Exp.t -> Sh.t
+val kill : Sh.t -> Var.t -> Sh.t
+val move : 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/solver.ml b/sledge/src/symbheap/solver.ml
index ecfb1db45..68ecaceb3 100644
--- a/sledge/src/symbheap/solver.ml
+++ b/sledge/src/symbheap/solver.ml
@@ -61,7 +61,7 @@ let single_existential_occurrence xs exp =
   with Multiple_existential_occurrences -> Many
 
 let special_cases xs = function
-  | Exp.(App {op= App {op= Eq; arg= Var _}; arg= Var _}) as e ->
+  | Exp.App {op= App {op= Eq; arg= Var _}; arg= Var _} as e ->
       if Set.is_subset (Exp.fv e) ~of_:xs then Exp.bool true else e
   | e -> e
 
diff --git a/sledge/src/symbheap/state_domain.ml b/sledge/src/symbheap/state_domain.ml
index f3bbac686..86a32746e 100644
--- a/sledge/src/symbheap/state_domain.ml
+++ b/sledge/src/symbheap/state_domain.ml
@@ -27,7 +27,8 @@ let init globals =
 let join = Sh.or_
 let is_false = Sh.is_false
 let exec_assume = Exec.assume
-let exec_return = Exec.return
+let exec_kill = Exec.kill
+let exec_move = Exec.move
 let exec_inst = Exec.inst
 let exec_intrinsic = Exec.intrinsic
 let dnf = Sh.dnf
@@ -66,46 +67,22 @@ let garbage_collect (q : t) ~wrt =
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp]
 
-type from_call = {subst: Var.Subst.t; frame: Sh.t}
+type from_call = {areturn: Var.t option; subst: Var.Subst.t; frame: Sh.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 temps and
-    fresh vars. *)
-let jump actuals formals ?temps q =
-  [%Trace.call fun {pf} ->
-    pf "@[<hv>actuals: (@[%a@])@ formals: (@[%a@])@ q: %a@]"
-      (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp)
-      (List.rev formals) Sh.pp q]
-  ;
-  let q', freshen_locals = Sh.freshen q ~wrt:(Var.Set.of_list formals) in
-  let and_eq q formal actual =
-    let actual' = Exp.rename freshen_locals actual in
-    Sh.and_ (Exp.eq (Exp.var formal) actual') q
-  in
-  let and_eqs formals actuals q =
-    List.fold2_exn ~f:and_eq formals actuals ~init:q
-  in
-  ( Option.fold ~f:(Fn.flip Sh.exists) temps
-      ~init:(and_eqs formals actuals q')
-  , {subst= freshen_locals; frame= Sh.emp} )
-  |>
-  [%Trace.retn fun {pf} (q', {subst}) ->
-    pf "@[<hv>subst: %a@ q': %a@]" Var.Subst.pp subst Sh.pp q']
-
 (** 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 fresh vars. *)
-let call ~summaries actuals formals locals globals q =
+let call ~summaries actuals areturn formals locals globals 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 pp q]
   ;
-  let wrt = Set.add_list formals locals in
-  let q', freshen_locals = Sh.freshen q ~wrt in
+  let q', freshen_locals =
+    Sh.freshen q ~wrt:(Set.add_list formals locals)
+  in
   let and_eq q formal actual =
     let actual' = Exp.rename freshen_locals actual in
     Sh.and_ (Exp.eq (Exp.var formal) actual') q
@@ -116,7 +93,7 @@ let call ~summaries actuals formals locals globals q =
   let q'' = and_eqs formals actuals q' in
   ( if not summaries then
     let q'' = Sh.extend_us locals q'' in
-    (q'', {subst= freshen_locals; frame= Sh.emp})
+    (q'', {areturn; subst= freshen_locals; frame= Sh.emp})
   else
     let formals_set = Var.Set.of_list formals in
     (* Add the formals here to do garbage collection and then get rid of
@@ -134,7 +111,7 @@ let call ~summaries actuals formals locals globals q =
         ~message:"Solver couldn't infer frame of a garbage-collected pre"
     in
     let q'' = Sh.extend_us locals (and_eqs formals actuals foot) in
-    (q'', {subst= freshen_locals; frame}) )
+    (q'', {areturn; subst= freshen_locals; frame}) )
   |>
   [%Trace.retn fun {pf} (q', {subst; frame}) ->
     pf "@[<v>subst: %a@ frame: %a@ q': %a@]" Var.Subst.pp subst pp frame pp
@@ -152,13 +129,19 @@ let post locals q =
 (** 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 {subst; frame} q =
+let retn formals freturn {areturn; subst; frame} q =
   [%Trace.call fun {pf} ->
     pf "@[<v>formals: {@[%a@]}@ subst: %a@ q: %a@ frame: %a@]"
       (List.pp ", " Var.pp) formals Var.Subst.pp (Var.Subst.invert subst) pp
       q pp frame]
   ;
-  let q = Sh.exists (Var.Set.of_list formals) q in
+  let q =
+    match (areturn, freturn) with
+    | Some areturn, Some freturn -> exec_move q areturn (Exp.var freturn)
+    | Some areturn, None -> exec_kill q areturn
+    | _ -> q
+  in
+  let q = Sh.exists (Set.add_list formals (Var.Set.of_option freturn)) q in
   let q = Sh.rename (Var.Subst.invert subst) q in
   Sh.star frame q
   |>
@@ -175,13 +158,12 @@ let pp_function_summary fs {xs; foot; post} =
   Format.fprintf fs "@[<v>xs: @[%a@]@ foot: %a@ post: %a @]" Var.Set.pp xs
     pp foot pp post
 
-let create_summary ~locals ~formals ~entry ~current =
+let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) =
   [%Trace.call fun {pf} ->
     pf "formals %a@ entry: %a@ current: %a" Var.Set.pp formals pp entry pp
-      current]
+      post]
   ;
   let foot = Sh.exists locals entry in
-  let post = Sh.exists locals current in
   let foot, subst = Sh.freshen ~wrt:(Set.union foot.us post.us) foot in
   let restore_formals q =
     Set.fold formals ~init:q ~f:(fun q var ->
@@ -199,7 +181,7 @@ let create_summary ~locals ~formals ~entry ~current =
   let xs_and_formals = Set.union xs formals in
   let foot = Sh.exists (Set.diff foot.us xs_and_formals) foot in
   let post = Sh.exists (Set.diff post.us xs_and_formals) post in
-  let current = Sh.extend_us xs current in
+  let current = Sh.extend_us xs post in
   ({xs; foot; post}, current)
   |>
   [%Trace.retn fun {pf} (fs, _) -> pf "@,%a" pp_function_summary fs]
diff --git a/sledge/src/symbheap/state_domain.mli b/sledge/src/symbheap/state_domain.mli
index fb7e044d5..e9ec91468 100644
--- a/sledge/src/symbheap/state_domain.mli
+++ b/sledge/src/symbheap/state_domain.mli
@@ -14,8 +14,9 @@ val init : Global.t vector -> t
 val join : t -> t -> t
 val is_false : t -> bool
 val exec_assume : t -> Exp.t -> t option
+val exec_kill : t -> Var.t -> t
+val exec_move : t -> Var.t -> Exp.t -> t
 val exec_inst : t -> Llair.inst -> (t, unit) result
-val exec_return : t -> Var.t -> Exp.t -> t
 
 val exec_intrinsic :
      skip_throw:bool
@@ -27,12 +28,10 @@ val exec_intrinsic :
 
 type from_call [@@deriving compare, equal, sexp]
 
-val jump :
-  Exp.t list -> Var.t list -> ?temps:Var.Set.t -> t -> t * from_call
-
 val call :
      summaries:bool
   -> Exp.t list
+  -> Var.t option
   -> Var.t list
   -> Var.Set.t
   -> Var.Set.t
@@ -54,7 +53,7 @@ val create_summary :
   -> function_summary * t
 
 val post : Var.Set.t -> t -> t
-val retn : Var.t list -> from_call -> t -> t
+val retn : Var.t list -> Var.t option -> from_call -> t -> t
 val dnf : t -> t list
 
 val resolve_callee :