diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index a708fbc01..8112f7b62 100644
--- a/sledge/src/control.ml
+++ b/sledge/src/control.ml
@@ -19,7 +19,7 @@ module Stack : sig
   val push_jump : Var.Set.t -> t -> t
 
   val push_call :
-       Var.Set.t
+       Llair.block
     -> retreating:bool
     -> bound:int
     -> return:Llair.jump
@@ -31,14 +31,14 @@ module Stack : sig
   val pop_return :
        t
     -> init:'a
-    -> f:(Var.Set.t -> Domain.from_call -> 'a -> 'b)
-    -> (t * 'b * Llair.jump) option
+    -> f:(Var.t option -> Var.Set.t -> Domain.from_call -> 'a -> 'a)
+    -> (Llair.jump * 'a * t) option
 
   val pop_throw :
        t
     -> init:'a
-    -> f:(Var.Set.t -> Domain.from_call -> 'a -> 'a)
-    -> (t * 'a * Llair.jump) option
+    -> f:(Var.t option -> Var.Set.t -> Domain.from_call -> 'a -> 'a)
+    -> (Llair.jump * 'a * t) option
 end = struct
   type t =
     | Locals of Var.Set.t * t
@@ -46,6 +46,8 @@ end = struct
         { retreating: bool
               (** return from a call not known to be nonrecursive *)
         ; dst: Llair.Jump.t
+        ; freturn: Var.t option
+        ; fthrow: Var.t
         ; from_call: Domain.from_call
         ; stk: t }
     | Throw of Llair.Jump.t * t
@@ -110,14 +112,16 @@ end = struct
     (if Set.is_empty lcls then stk else Locals (lcls, stk))
     |> check invariant
 
-  let push_return ~retreating dst from_call stk =
-    Return {retreating; dst; from_call; 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_throw jmp stk =
     (match jmp with None -> stk | Some jmp -> Throw (jmp, stk))
     |> check invariant
 
-  let push_call locals ~retreating ~bound ~return from_call ?throw stk =
+  let push_call {Llair.locals; parent= {freturn; fthrow}} ~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
@@ -132,7 +136,8 @@ end = struct
     else
       Some
         (push_jump locals
-           (push_throw throw (push_return ~retreating return from_call stk)))
+           (push_throw throw
+              (push_return ~retreating return freturn fthrow from_call stk)))
     )
     |>
     [%Trace.retn fun {pf} _ ->
@@ -142,8 +147,13 @@ end = struct
     let rec pop_return_ scope = function
       | Locals (locals, stk) -> pop_return_ (Set.union locals scope) stk
       | Throw (_, stk) -> pop_return_ scope stk
-      | Return {dst; from_call; stk} ->
-          Some (stk, f scope from_call init, dst)
+      | 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)
       | Empty -> None
     in
     pop_return_ Var.Set.empty stk
@@ -152,10 +162,11 @@ end = struct
     let rec pop_throw_ scope state = function
       | Locals (locals, stk) ->
           pop_throw_ (Set.union locals scope) state stk
-      | Return {from_call; stk} ->
-          pop_throw_ Var.Set.empty (f scope from_call state) stk
-      | Throw (jmp, Return {from_call; stk}) ->
-          Some (stk, f scope from_call state, jmp)
+      | 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)
       | Empty -> None
       | Throw _ as stk -> violates invariant stk
     in
@@ -269,30 +280,29 @@ let exec_goto stk state block ({dst; retreating} : Llair.jump) =
   Work.add ~prev:block ~retreating stk state dst
 
 let exec_jump stk state block ({dst; args} as jmp : Llair.jump) =
-  let state, _ = Domain.call state args dst.params dst.locals in
+  let state, _ = Domain.call args dst.params dst.locals state in
   exec_goto stk state block jmp
 
 let exec_call ~opts stk state block ({dst; args; retreating} : Llair.jump)
     return throw =
-  let state, from_call = Domain.call state args dst.params dst.locals in
+  let state, from_call = Domain.call args dst.params dst.locals state in
   match
-    Stack.push_call ~bound:opts.bound dst.locals ~retreating ~return
-      from_call ?throw stk
+    Stack.push_call ~bound:opts.bound dst ~retreating ~return from_call
+      ?throw stk
   with
   | Some stk -> Work.add stk ~prev:block ~retreating state dst
   | None -> Work.skip
 
-let exec_return stk state block exp =
-  match Stack.pop_return stk ~init:state ~f:Domain.retn with
-  | Some (stk, state, ({args} as jmp)) ->
-      exec_jump stk state block {jmp with args= Option.cons exp args}
+let exec_pop pop stk state block exp =
+  match pop stk ~init:state ~f:(Domain.retn exp) with
+  | Some (jmp, state, stk) -> exec_jump stk state block jmp
   | None -> Work.skip
 
+let exec_return stk state block exp =
+  exec_pop Stack.pop_return stk state block exp
+
 let exec_throw stk state block exc =
-  match Stack.pop_throw stk ~init:state ~f:Domain.retn with
-  | Some (stk, state, ({args} as jmp)) ->
-      exec_jump stk state block {jmp with args= exc :: args}
-  | None -> Work.skip
+  exec_pop Stack.pop_throw stk state block (Some exc)
 
 let exec_skip_func :
     Stack.t -> Domain.t -> Llair.block -> Llair.jump -> Work.x =
@@ -405,7 +415,7 @@ let harness : Llair.t -> (int -> Work.t) option =
   | Some {entry= {params= []} as block} ->
       Some
         (Work.init
-           (fst (Domain.call (Domain.init pgm.globals) [] [] block.locals))
+           (fst (Domain.call [] [] block.locals (Domain.init pgm.globals)))
            block)
   | _ -> None
 
diff --git a/sledge/src/import/import.ml b/sledge/src/import/import.ml
index ee57eb87a..61f6f2f63 100644
--- a/sledge/src/import/import.ml
+++ b/sledge/src/import/import.ml
@@ -262,6 +262,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_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)
   let of_vector cmp x = of_array cmp (Vector.to_array x)
diff --git a/sledge/src/import/import.mli b/sledge/src/import/import.mli
index 05efd2b75..de9ecf007 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_list : 'e list -> ('e, 'c) t -> ('e, 'c) t
 
   val diff_inter_diff :
     ('e, 'c) t -> ('e, 'c) t -> ('e, 'c) t * ('e, 'c) t * ('e, 'c) t
diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml
index 00edb1d44..1690a485e 100644
--- a/sledge/src/llair/llair.ml
+++ b/sledge/src/llair/llair.ml
@@ -56,7 +56,12 @@ and cfg = block vector
 (* [entry] is not part of [cfg] since it is special in several ways: its
    params are the func params, its locals are all the locals in it plus the
    cfg, and it cannot be jumped to, only called. *)
-and func = {name: Global.t; entry: block; cfg: cfg}
+and func =
+  { name: Global.t
+  ; entry: block
+  ; cfg: cfg
+  ; freturn: Var.t option
+  ; fthrow: Var.t }
 
 let sexp_cons (hd : Sexp.t) (tl : Sexp.t) =
   match tl with
@@ -201,10 +206,13 @@ let rec dummy_block =
   ; sort_index= 0 }
 
 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 (Var.program "dummy") dummy_ptr_typ Loc.none
+  { name= Global.mk dummy_var dummy_ptr_typ Loc.none
   ; entry= dummy_block
-  ; cfg= Vector.empty }
+  ; cfg= Vector.empty
+  ; freturn= None
+  ; fthrow= dummy_var }
 
 (** Instructions *)
 
@@ -416,13 +424,25 @@ module Func = struct
 
   let find functions name = Map.find functions name
 
-  let mk ~name ~entry ~cfg =
+  let mk ~(name : Global.t) ~entry ~cfg =
     let locals =
       Vector.fold ~init:entry.locals cfg ~f:(fun locals block ->
           Set.union locals block.locals )
     in
+    let freturn, locals =
+      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)
+    in
     let entry = {entry with locals} in
-    let func = {name; entry; cfg} in
+    let func = {name; entry; cfg; freturn; fthrow} in
     let resolve_parent_and_jumps block =
       block.parent <- func ;
       let lookup cfg lbl : block =
diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli
index 9be5956b2..161ce284d 100644
--- a/sledge/src/llair/llair.mli
+++ b/sledge/src/llair/llair.mli
@@ -107,7 +107,12 @@ and cfg
 
 (** A function is a control-flow graph with distinguished entry block, whose
     parameters are the function parameters. *)
-and func = private {name: Global.t; entry: block; cfg: cfg}
+and func = private
+  { name: Global.t
+  ; entry: block
+  ; cfg: cfg
+  ; freturn: Var.t option
+  ; fthrow: Var.t }
 
 type functions
 
diff --git a/sledge/src/symbheap/domain.ml b/sledge/src/symbheap/domain.ml
index c0ab083ca..997ca26a3 100644
--- a/sledge/src/symbheap/domain.ml
+++ b/sledge/src/symbheap/domain.ml
@@ -29,7 +29,7 @@ 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 q actuals formals locals =
+let call actuals formals locals q =
   [%Trace.call fun {pf} ->
     pf
       "@[<hv>actuals: (@[%a@])@ formals: (@[%a@])@ locals: {@[%a@]}@ q: %a@]"
@@ -52,14 +52,25 @@ let call q actuals formals locals =
 (** 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 locals freshen_locals q =
+let retn actual formal locals freshen_locals q =
   [%Trace.call fun {pf} ->
-    pf "@[<hv>locals: {@[%a@]}@ subst: %a@ q: %a@]" Var.Set.pp locals
-      Var.Subst.pp
+    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
       (Var.Subst.invert freshen_locals)
       Sh.pp q]
   ;
-  Sh.rename (Var.Subst.invert freshen_locals) (Sh.exists locals 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')
   |>
   [%Trace.retn fun {pf} -> pf "%a" Sh.pp]
 
diff --git a/sledge/src/symbheap/domain.mli b/sledge/src/symbheap/domain.mli
index dab5e3182..01ae1c942 100644
--- a/sledge/src/symbheap/domain.mli
+++ b/sledge/src/symbheap/domain.mli
@@ -20,8 +20,8 @@ val exec_intrinsic :
 
 type from_call [@@deriving compare, equal, sexp]
 
-val call : t -> Exp.t list -> Var.t list -> Var.Set.t -> t * from_call
-val retn : Var.Set.t -> from_call -> 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 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 01806ecfb..7b2482789 100644
--- a/sledge/src/symbheap/exec.ml
+++ b/sledge/src/symbheap/exec.ml
@@ -571,7 +571,7 @@ let strlen_spec us reg ptr =
 (* execute a command with given spec from pre *)
 let exec_spec pre {xs; foot; post} =
   [%Trace.call fun {pf} ->
-    pf "@[%a@]@ @[<2>%a@\n@[<hv>{%a  }@;<1 -1>--@ {%a  }@]@]" Sh.pp pre
+    pf "@[%a@]@ @[<2>%a@,@[<hv>{%a  }@;<1 -1>--@ {%a  }@]@]" Sh.pp pre
       (Sh.pp_us ~pre:"@<2>∀ ")
       xs Sh.pp foot Sh.pp post ;
     assert (
diff --git a/sledge/test/exec/wrap_malloc.c b/sledge/test/exec/wrap_malloc.c
new file mode 100644
index 000000000..d07829b24
--- /dev/null
+++ b/sledge/test/exec/wrap_malloc.c
@@ -0,0 +1,14 @@
+/*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+#include <stdlib.h>
+
+char* c() { return malloc(12); }
+int main() {
+  char* s = c();
+  return s ? *s : 1;
+}
diff --git a/sledge/test/report.expected b/sledge/test/report.expected
index 90902b711..8d848d5b6 100644
--- a/sledge/test/report.expected
+++ b/sledge/test/report.expected
@@ -3,6 +3,7 @@ frontend/cond_alloca.bc:	RESULT: Internal error: no applicable harness
 exec/globals.bc:	RESULT: Success
 exec/global_vars.bc:	RESULT: Success
 exec/recursion.bc:	RESULT: Success
+exec/wrap_malloc.bc:	RESULT: Success
 frontend/destructor_bases.bc:	RESULT: Success
 frontend/exceptions.bc:	RESULT: Success
 frontend/rethrow.bc:	RESULT: Success