diff --git a/examples/memory/memory_interproc.il b/examples/memory/memory_interproc.il
new file mode 100644
index 00000000..c50d5d9c
--- /dev/null
+++ b/examples/memory/memory_interproc.il
@@ -0,0 +1,40 @@
+memory shared $mem : (bv64 -> bv8);
+memory $stack : (bv64 -> bv8);
+
+prog entry @main;
+
+proc @malloc(R0_in:bv64) -> (R0_out:bv64);
+proc @free(R0_in:bv64) -> ();
+
+// In future, realloc should actually copy the byte accross.
+// For now that is ommitted from this test as the store expression
+// locks up the interprocedural redundancy check forever.
+proc @realloc(ptr_in:bv64) -> (ptr_out:bv64)
+[
+    block %realloc [
+        // var x:bv8 := load le $mem ptr_in 8;
+        call @free(ptr_in);
+        var size: bv64 := 1:bv64;
+        var (ptr_out:bv64) := call @malloc(size);
+        // store le $mem ptr_out x 8;
+        goto(%realloc_return);
+    ];
+    block %realloc_return [
+        return;
+    ];
+];
+
+proc @main () -> ()
+[
+    block %main_entry [
+        var size: bv64 := 1:bv64;
+        var (addr:bv64) := call @malloc(size);
+        var (addr_2:bv64) := call @realloc(addr);
+        goto(%main_return);
+    ];
+    block %main_return [
+        assert neq(addr, addr_2);
+        call @free(addr_2);
+        return;
+    ];
+];
diff --git a/examples/memory/memory_safety.il b/examples/memory/memory_safety.il
new file mode 100644
index 00000000..b7d36b59
--- /dev/null
+++ b/examples/memory/memory_safety.il
@@ -0,0 +1,121 @@
+memory shared $mem : (bv64 -> bv8);
+memory $stack : (bv64 -> bv8);
+
+prog entry @main;
+
+// Unspecified malloc/free procedures. Specified by
+// memory specification + encoding transform.
+proc @malloc(R0_in:bv64) -> (R0_out:bv64);
+proc @free(R0_in:bv64) -> ();
+
+// Valid memory operations. Allocates 2 bytes,
+// stores/loads to the allocated space, and frees.
+proc @main () -> () { .entrypoint=true; }
+[
+    block %main_entry [
+        var size:bv64 := 2:bv64;
+        var (addr:bv64) := call @malloc(size);
+
+        store le $mem bvadd(addr,0:bv64) 0xff:bv8 8;
+        var temp:bv8 := load le $mem bvadd(addr,0:bv64) 8;
+
+        call @free(addr);
+
+        goto(%main_return);
+    ];
+    block %main_return [
+        return ();
+    ];
+];
+
+// Double free example. Calls free on address twice.
+proc @double_free () -> () { .entrypoint=true; }
+[
+    block %main_entry [
+        var size:bv64 := 2:bv64;
+        var (addr:bv64) := call @malloc(size);
+
+        store le $mem bvadd(addr,0:bv64) 0xff:bv8 8;
+        var temp:bv8 := load le $mem bvadd(addr,0:bv64) 8;
+
+        call @free(addr);
+        call @free(addr);
+
+        goto(%main_return);
+    ];
+    block %main_return [
+        return ();
+    ];
+];
+
+// Example of freeing a valid address which is not at the
+// base of an allocation.
+proc @invalid_free () -> () { .entrypoint=true; }
+[
+    block %main_entry [
+        var size:bv64 := 2:bv64;
+        var (addr:bv64) := call @malloc(size);
+
+        call @free(bvadd(addr,1:bv64));
+
+        goto(%main_return);
+    ];
+    block %main_return [
+        return ();
+    ];
+];
+
+// Example of loading memory after free.
+proc @use_after_free () -> () { .entrypoint=true; }
+[
+    block %main_entry [
+        var size:bv64 := 2:bv64;
+        var (addr:bv64) := call @malloc(size);
+
+        store le $mem bvadd(addr,0:bv64) 0xff:bv8 8;
+        call @free(addr);
+        var temp:bv8 := load le $mem bvadd(addr,0:bv64) 8;
+
+        goto(%main_return);
+    ];
+    block %main_return [
+        return ();
+    ];
+];
+
+// Example reading at offset 4 of a 2 byte allocation.
+proc @out_of_bounds () -> () { .entrypoint=true; }
+[
+    block %main_entry [
+        var size:bv64 := 2:bv64;
+        var (addr:bv64) := call @malloc(size);
+
+        store le $mem bvadd(addr,4:bv64) 0xff:bv8 8;
+        var temp:bv8 := load le $mem bvadd(addr,4:bv64) 8;
+
+        call @free(addr);
+
+        goto(%main_return);
+    ];
+    block %main_return [
+        return ();
+    ];
+];
+
+// Example of catching a memory leak (unfreed addr).
+proc @memory_leak () -> () { .entrypoint=true; }
+[
+    block %main_entry [
+        var size:bv64 := 2:bv64;
+        var (addr:bv64) := call @malloc(size);
+
+        store le $mem bvadd(addr,0:bv64) 0xff:bv8 8;
+        var temp:bv8 := load le $mem bvadd(addr,0:bv64) 8;
+
+        goto(%main_return);
+    ];
+    block %main_return [
+        return ();
+    ];
+];
+
diff --git a/flake.nix b/flake.nix
index db41d021..d2504742 100644
--- a/flake.nix
+++ b/flake.nix
@@ -90,8 +90,14 @@
 
           devShells = {
             default = self.devShells.fp;
-            fp = fpOcamlPackages.callPackage ./nix/shell.nix { inherit bnfc-treesitter; };
-            no-fp = selfOcamlPackages.callPackage ./nix/shell.nix { inherit bnfc-treesitter; };
+            fp = fpOcamlPackages.callPackage ./nix/shell.nix {
+              inherit bnfc-treesitter;
+              z3 = pkgs.z3.out;
+            };
+            no-fp = selfOcamlPackages.callPackage ./nix/shell.nix {
+              inherit bnfc-treesitter;
+              z3 = pkgs.z3.out;
+            };
           };
         };
     };
diff --git a/lib/analysis/dataflow_graph.ml b/lib/analysis/dataflow_graph.ml
index 184a7e63..89de1e70 100644
--- a/lib/analysis/dataflow_graph.ml
+++ b/lib/analysis/dataflow_graph.ml
@@ -540,7 +540,7 @@ struct
 
     include SV
 
-    let init p =
+    let init ?(vertex = None) p =
       let vs = Lang.Procedure.formal_in_params p |> StringMap.values in
       vs
       |> Iter.map (fun v -> (v, top_val))
diff --git a/lib/analysis/dune b/lib/analysis/dune
index 13dcefb1..2db2123c 100644
--- a/lib/analysis/dune
+++ b/lib/analysis/dune
@@ -18,6 +18,7 @@
   tnum_wint_reduced_product
   known_bits
   wp_dual
+  sp
   sva)
  (libraries
   intPQueue
diff --git a/lib/analysis/gamma_domain.ml b/lib/analysis/gamma_domain.ml
index fbea8a4c..47667b18 100644
--- a/lib/analysis/gamma_domain.ml
+++ b/lib/analysis/gamma_domain.ml
@@ -22,7 +22,7 @@ module Domain = struct
 
   let name = "Gamma domain"
 
-  let init proc =
+  let init ?(vertex = None) proc =
     Procedure.formal_in_params proc
     |> StringMap.values
     |> Iter.append
diff --git a/lib/analysis/intra_analysis.ml b/lib/analysis/intra_analysis.ml
index 0255a4d5..cd8b34a4 100644
--- a/lib/analysis/intra_analysis.ml
+++ b/lib/analysis/intra_analysis.ml
@@ -169,7 +169,7 @@ module Forwards (D : IntraDomain) = struct
         Procedure.graph p
         |> Option.map (fun g ->
             A.recurse g (Procedure.topo_fwd p)
-              (fun v -> D.init p)
+              (fun v -> D.init ~vertex:(Some v) p)
               widening_set widening_delay))
     |> Option.get_or ~default:A.M.empty
 
diff --git a/lib/analysis/known_bits.ml b/lib/analysis/known_bits.ml
index 68db2c89..5319a827 100644
--- a/lib/analysis/known_bits.ml
+++ b/lib/analysis/known_bits.ml
@@ -274,7 +274,7 @@ module Domain = struct
 
   include StateAbstraction
 
-  let init p =
+  let init ?(vertex = None) p =
     let vs = Lang.Procedure.formal_in_params p |> StringMap.values in
     vs
     |> Iter.map (fun v -> (v, top_val))
diff --git a/lib/analysis/lattice_types.ml b/lib/analysis/lattice_types.ml
index d362fbb2..d1d2c0cc 100644
--- a/lib/analysis/lattice_types.ml
+++ b/lib/analysis/lattice_types.ml
@@ -85,7 +85,7 @@ end
 module type StateDomain = sig
   include StateAbstraction
 
-  val init : Program.proc -> t
+  val init : ?vertex:Procedure.Vert.t Option.t -> Program.proc -> t
   val transfer_state : (Var.t -> V.t) -> Program.stmt -> (Var.t * V.t) Iter.t
 end
 
@@ -93,7 +93,7 @@ module type Domain = sig
   include Lattice
 
   val transfer : t -> Program.stmt -> t
-  val init : Program.proc -> t
+  val init : ?vertex:Procedure.Vert.t Option.t -> Program.proc -> t
 end
 
 module FlatLattice (L : sig
diff --git a/lib/analysis/sp.ml b/lib/analysis/sp.ml
new file mode 100644
index 00000000..9f8e614e
--- /dev/null
+++ b/lib/analysis/sp.ml
@@ -0,0 +1,261 @@
+(* The sp domain for postcondition inference *)
+(* Assumes SSA form *)
+
+open Lang
+open Common
+open Expr
+
+module type FunctionAnnotation = sig
+  val requires : ID.t -> Expr.BasilExpr.t list
+  val ensures : ID.t -> Expr.BasilExpr.t list
+  val inout : ID.t -> VarSet.t
+  val id : ID.t
+end
+
+let expr_size e =
+  let open AbstractExpr in
+  let alg (e : int BasilExpr.abstract_expr) =
+    (match e with
+      | RVar { attrib; id } -> 0
+      | Constant { attrib; const } -> 0
+      | UnaryExpr { attrib; op; arg } -> arg
+      | BinaryExpr { attrib; op; arg1; arg2 } -> arg1 + arg2
+      | ApplyIntrin { attrib; op; args } -> List.fold_left ( + ) 0 args
+      | ApplyFun { attrib; func; args } -> func + List.fold_left ( + ) 0 args
+      | Lambda { op; attrib; bound_vars; in_body } -> in_body
+      | Let { attrib; bound_vars; in_body } -> in_body)
+    + 1
+  in
+  BasilExpr.cata alg e
+
+module Domain (S : FunctionAnnotation) = struct
+  let name = "SP domain"
+
+  type t = Program.e
+
+  let e_true = BasilExpr.boolconst true
+  let e_false = BasilExpr.boolconst false
+
+  let simplify =
+    let open AbstractExpr in
+    let open BasilExpr in
+    let rw =
+      BasilExpr.rewrite ~rw_fun:(function
+        | ApplyIntrin { op; args = [ l ] } -> replace [%here] l
+        | ApplyIntrin { attrib; op = `OR; args }
+          when List.mem ~eq:BasilExpr.equal e_false args ->
+            let args = List.remove ~eq:BasilExpr.equal ~key:e_false args in
+            replace [%here]
+              (match args with
+              | [] -> e_false
+              | [ l ] -> l
+              | args -> BasilExpr.fix (ApplyIntrin { attrib; op = `OR; args }))
+        | ApplyIntrin { attrib; op = `AND; args }
+          when List.mem ~eq:BasilExpr.equal e_true args ->
+            let args = List.remove ~eq:BasilExpr.equal ~key:e_true args in
+            replace [%here]
+              (match args with
+              | [] -> e_true
+              | [ l ] -> l
+              | args -> BasilExpr.fix (ApplyIntrin { attrib; op = `AND; args }))
+        | ApplyIntrin { op = `OR; args }
+          when List.mem ~eq:BasilExpr.equal e_true args ->
+            replace [%here] e_true
+        | ApplyIntrin { op = `AND; args }
+          when List.mem ~eq:BasilExpr.equal e_false args ->
+            replace [%here] e_false
+        | BinaryExpr { op = `EQ; arg1; arg2 } when BasilExpr.equal arg1 arg2 ->
+            replace [%here] e_true
+        | UnaryExpr { op = `BoolNOT; arg } when BasilExpr.equal arg e_true ->
+            replace [%here] e_false
+        | UnaryExpr { attrib; op = `Gamma; arg } ->
+            replace [%here]
+              (match free_vars arg |> VarSet.to_list with
+              | [] -> e_true
+              | [ v ] -> unexp ~op:`Gamma @@ rvar v
+              | vars ->
+                  BasilExpr.fix
+                    (ApplyIntrin
+                       {
+                         attrib;
+                         op = `AND;
+                         args =
+                           vars
+                           |> List.map
+                                (BasilExpr.unexp ~op:`Gamma % BasilExpr.rvar);
+                       }))
+        | _ -> Keep)
+    in
+    rw % rw
+
+  let show = BasilExpr.to_string
+  let equal = BasilExpr.equal
+  let compare = BasilExpr.compare
+  let pretty = BasilExpr.pretty
+  let top = e_true
+  let bottom = e_false
+  let join (a : t) (b : t) : t = BasilExpr.applyintrin ~op:`OR [ a; b ]
+  let leq a b = failwith "leq not implemented"
+  let widening a b = top
+
+  let locals (p : BasilExpr.t) =
+    BasilExpr.free_vars p
+    |> flip VarSet.diff (S.inout S.id)
+    |> VarSet.filter (fun v -> not @@ Var.is_global v)
+
+  let substitute_var_names (a : (string * BasilExpr.t) list) (p : BasilExpr.t) :
+      BasilExpr.t =
+    BasilExpr.substitute
+      (fun v ->
+        List.find_map
+          (fun (v', e) -> Option.return_if (String.equal (Var.name v) v') e)
+          a)
+      p
+    |> simplify
+
+  let conjunction ls = BasilExpr.applyintrin ~op:`AND ls
+
+  let tf_assigns p a =
+    a
+    |> List.map (function a, b -> BasilExpr.binexp ~op:`EQ (BasilExpr.rvar a) b)
+    |> List.fold_left (fun a p -> conjunction [ a; p ]) p
+    |> simplify
+
+  let transfer (p : t) (stmt : Program.stmt) : t =
+    match stmt with
+    | Instr_Assign [] -> p
+    | Instr_Assign (a : (Var.t * BasilExpr.t) list) ->
+        tf_assigns p a |> simplify
+    | Instr_Assume { body; branch = false } -> conjunction [ p; simplify body ]
+    | Instr_Assert { body } -> conjunction [ p; simplify body ]
+    | Instr_Call { lhs; procid; args } ->
+        let sub (s : BasilExpr.t) : BasilExpr.t =
+          s
+          |> substitute_var_names (StringMap.to_list args)
+          |> substitute_var_names
+               (StringMap.to_list lhs
+               |> List.map (fun (i, v) -> (i, BasilExpr.rvar v)))
+        in
+        let r = conjunction @@ (e_true :: (S.ensures procid |> List.map sub)) in
+        conjunction [ p; simplify r ]
+    | Instr_Store
+        {
+          lhs;
+          rhs;
+          value;
+          addr = Addr { addr : 'e; size : int; endian : Stmt.endian };
+        } ->
+        conjunction
+          [
+            p;
+            BasilExpr.binexp ~op:`EQ value
+              (BasilExpr.binexp
+                 ~op:(`Load (endian, size))
+                 (BasilExpr.rvar lhs) addr);
+          ]
+    | Instr_Load
+        {
+          lhs;
+          rhs;
+          addr = Addr { addr : 'e; size : int; endian : Stmt.endian };
+        } ->
+        (* Without a load expression it is unclear what to constrain here. *)
+        (* Could be a map access in future. *)
+        top
+    | Instr_IndirectCall _ | Instr_IntrinCall _ -> top
+    | _ -> top
+
+  let init ?(vertex = None) (proc : Program.proc) : t =
+    match vertex with Some Procedure.Vert.Entry -> top | _ -> bottom
+
+  let transfer_phi (m : t) (p : Var.t Block.phi) : t =
+    match p with
+    | { lhs; rhs } ->
+        let rhs =
+          List.map (fun (_, v) -> tf_assigns m [ (lhs, BasilExpr.rvar v) ]) rhs
+        in
+        List.fold_left join bottom rhs
+
+  let to_pred (p : t) : BasilExpr.t =
+    let l = locals p in
+    match VarSet.cardinal l with
+    | 0 -> p
+    | _ ->
+        if expr_size p > 10000 then BasilExpr.boolconst true
+        else
+          BasilExpr.exists ~bound:(VarSet.to_list @@ l) p
+          |> Algsimp.Comb.to_steady Expr.BasilExpr.equal
+               Algsimp.alg_simp_rewriter
+end
+
+let%expect_test "sp" =
+  let prog =
+    (Loader.Loadir.ast_of_string
+       {|
+proc @branching(a:bv64) -> (b:bv64) [
+   block %1 [ goto (%2); ];
+   block %2 [
+     var a_1:bv64 := a:bv64;
+     assume bvult(a_1:bv64, 0x64:bv64);
+     goto (%3_2,%3_1);
+   ];
+   block %3_1 [
+     var a_3:bv64 := a_1:bv64;
+     assume bvult(a_3:bv64, 0x32:bv64);
+     var x_2:bv64 := a_3:bv64;
+     goto (%4);
+   ];
+   block %3_2 [
+     var a_2:bv64 := a_1:bv64;
+     assume boolnot(bvult(a_2:bv64, 0x32:bv64));
+     var x_1:bv64 := 0x0:bv64;
+     goto (%4);
+   ];
+   block %4 ( var x_3:bv64 := phi(%3_2 -> x_1:bv64, %3_1 -> x_2:bv64) ) [
+     var b:bv64 := x_3:bv64;
+     return;
+   ]
+];
+    |})
+      .prog
+  in
+  let module IntraDomain = Domain (struct
+    let requires = const []
+    let ensures = const []
+
+    let inout id =
+      Program.proc_opt prog id
+      |> Option.map_or
+           (fun p ->
+             VarSet.union
+               (VarSet.of_iter @@ StringMap.values
+               @@ Procedure.formal_in_params p)
+               (VarSet.of_iter @@ StringMap.values
+               @@ Procedure.formal_out_params p))
+           ~default:VarSet.empty
+
+    let id = Procedure.id @@ Program.get_proc_by_name "@branching" prog
+  end) in
+  let module IntraAnalysis = Intra_analysis.Forwards (IntraDomain) in
+  let proc = Program.get_proc_by_name "@branching" prog in
+  let res =
+    IntraAnalysis.analyse ~widening_set:Graph.ChaoticIteration.FromWto
+      ~widening_delay:5 proc
+  in
+  IntraAnalysis.A.M.find Procedure.Vert.Return res
+  |> IntraDomain.to_pred |> BasilExpr.to_string |> print_endline;
+  [%expect
+    {|
+    exists (a_1:bv64) (a_3:bv64) (x_2:bv64) (a_2:bv64) (x_1:bv64) (x_3:bv64) :: (boolor(booland(boolor(booland(boolor(booland(eq(a_1:bv64,
+            a:bv64), bvult(a_1:bv64, 0x64:bv64), eq(a_3:bv64, a_1:bv64),
+           bvult(a_3:bv64, 0x32:bv64), eq(x_2:bv64, a_3:bv64)),
+          booland(eq(a_1:bv64, a:bv64), bvult(a_1:bv64, 0x64:bv64),
+           eq(a_2:bv64, a_1:bv64), boolnot(bvult(a_2:bv64, 0x32:bv64)),
+           eq(x_1:bv64, 0x0:bv64))), eq(x_3:bv64, x_1:bv64)),
+        booland(boolor(booland(eq(a_1:bv64, a:bv64), bvult(a_1:bv64, 0x64:bv64),
+           eq(a_3:bv64, a_1:bv64), bvult(a_3:bv64, 0x32:bv64), eq(x_2:bv64, a_3:bv64)),
+          booland(eq(a_1:bv64, a:bv64), bvult(a_1:bv64, 0x64:bv64),
+           eq(a_2:bv64, a_1:bv64), boolnot(bvult(a_2:bv64, 0x32:bv64)),
+           eq(x_1:bv64, 0x0:bv64))), eq(x_3:bv64, x_2:bv64))), eq(b:bv64, x_3:bv64)),
+      false, false))
+    |}]
diff --git a/lib/analysis/sva.ml b/lib/analysis/sva.ml
index 6517ae13..84e798c5 100644
--- a/lib/analysis/sva.ml
+++ b/lib/analysis/sva.ml
@@ -63,7 +63,7 @@ module IntervalDomain = struct
   let join = WrappedIntervalsLattice.join
   let top = WrappedIntervalsLattice.Top
   let neg = WrappedIntervalsLatticeOps.neg
-  let init a = interval a a
+  let init ?(vertex = None) a = interval a a
 end
 
 module SymAddrSetLattice = struct
@@ -172,7 +172,7 @@ module Domain = struct
     List.init 11 (fun i -> 19 + i) |> fun lst ->
     31 :: lst |> List.map (fun i -> "R" ^ string_of_int i)
 
-  let init proc =
+  let init ?(vertex = None) proc =
     let open Option in
     let name = ID.name @@ Procedure.id proc in
     StringMap.filter (fun param _ ->
diff --git a/lib/analysis/tnum_wint_reduced_product.ml b/lib/analysis/tnum_wint_reduced_product.ml
index 5338e75e..351062cf 100644
--- a/lib/analysis/tnum_wint_reduced_product.ml
+++ b/lib/analysis/tnum_wint_reduced_product.ml
@@ -167,7 +167,7 @@ module Domain = struct
 
   let top_val = TnumWintReducedProductLattice.top
 
-  let init p =
+  let init ?(vertex = None) p =
     let vs = Lang.Procedure.formal_in_params p |> StringMap.values in
     vs
     |> Iter.map (fun v -> (v, top_val))
diff --git a/lib/analysis/wp_dual.ml b/lib/analysis/wp_dual.ml
index 24fd8332..0af998d2 100644
--- a/lib/analysis/wp_dual.ml
+++ b/lib/analysis/wp_dual.ml
@@ -1,15 +1,16 @@
 (* The wp dual domain for precondition inference *)
+(* Assumes SSA form *)
 
 open Lang
 open Common
 open Expr
 
-module type FunctionSummaryAnnotation = sig
+module type FunctionAnnotation = sig
   val requires : ID.t -> Expr.BasilExpr.t list
   val ensures : ID.t -> Expr.BasilExpr.t list
 end
 
-module Domain (S : FunctionSummaryAnnotation) = struct
+module Domain (S : FunctionAnnotation) = struct
   let name = "WP dual domain"
 
   type t = Program.e
@@ -79,7 +80,7 @@ module Domain (S : FunctionSummaryAnnotation) = struct
 
   let join a b = BasilExpr.applyintrin ~op:`OR [ a; b ] |> simplify
   let widening a b = top
-  let init proc = bottom
+  let init ?(vertex = None) proc = bottom
 
   let leq a b =
     raise
diff --git a/lib/analysis/wrapped_intervals.ml b/lib/analysis/wrapped_intervals.ml
index 1ac01bc1..1963b60e 100644
--- a/lib/analysis/wrapped_intervals.ml
+++ b/lib/analysis/wrapped_intervals.ml
@@ -777,7 +777,7 @@ module Domain = struct
 
   let top_val = WrappedIntervalsLattice.top
 
-  let init p =
+  let init ?(vertex = None) p =
     let vs = Lang.Procedure.formal_in_params p |> StringMap.values in
     vs
     |> Iter.map (fun v -> (v, top_val))
diff --git a/lib/lang/expr.ml b/lib/lang/expr.ml
index b45de43e..6bb59d41 100644
--- a/lib/lang/expr.ml
+++ b/lib/lang/expr.ml
@@ -505,7 +505,7 @@ module BasilExpr = struct
         let binding =
           fill (text " ")
             (List.map (fun v -> bracket "(" (Var.pretty v) ")") bound_vars)
-          ^+ sep ^+ a ^ bracket "(" b ")"
+          ^+ sep ^+ bracket "(" b ")"
         in
         return (text op ^ a ^ text " " ^ binding)
     | Lambda { bound_vars; in_body; attrib } -> pass ()
diff --git a/lib/transforms/boogie_prepass.ml b/lib/transforms/boogie_prepass.ml
index 4debcc98..ff040a37 100644
--- a/lib/transforms/boogie_prepass.ml
+++ b/lib/transforms/boogie_prepass.ml
@@ -178,23 +178,39 @@ module Builtins = struct
         : Program.declaration)
 
   let used_ops (p : Program.t) =
-    Iter.from_iter (fun f -> iprog f p)
-    |> Iter.sort_uniq
+    Iter.from_iter (fun f -> iprog f p) |> Iter.sort_uniq
+
+  let transform_add_builtin_decls (p : Program.t) : Program.t =
+    used_ops p
     |> Iter.filter_map (function op, args, ret ->
         (match op with
+        | `Load _ -> None
         | #builtin as op -> transform_op_to_decl op args ret
         | _ -> None))
     |> Iter.to_list
-
-  let transform_add_builtin_decls (p : Program.t) : Program.t =
-    used_ops p |> List.fold_left Program.add_decl p
+    |> List.fold_left Program.add_decl p
 end
 
 module Instructions = struct
   let unique_stores_loads (prog : Program.t) =
     let visit_procs proc = Procedure.iter_stmt_topo_fwd proc in
+    let load_exprs : (Var.t, Var.t, Program.e) Stmt.t Iter.t =
+      Builtins.used_ops prog
+      |> Iter.filter_map (function op, args, ret ->
+          (match op with
+          | `Load (endian, size) ->
+              let lhs = Var.create "" ret in
+              let rhs = Var.create "" (List.hd args) in
+              let addr =
+                Expr.BasilExpr.rvar @@ Var.create "" (List.hd @@ List.tl args)
+              in
+              Some
+                (Stmt.Instr_Load
+                   { lhs; rhs; addr = Addr { addr; size; endian } })
+          | _ -> None))
+    in
     let procs = Program.procs prog |> Iter.map snd in
-    procs |> Iter.flat_map visit_procs
+    procs |> Iter.flat_map visit_procs |> Iter.append load_exprs
     |> Iter.filter (function
       | Stmt.Instr_Store { lhs; rhs; value; addr = Scalar } -> true
       | Stmt.Instr_Store { lhs; rhs; value; addr = Addr { addr; size; endian } }
diff --git a/lib/transforms/function_summaries.ml b/lib/transforms/function_summaries.ml
index 36ea8bad..cd0a4d38 100644
--- a/lib/transforms/function_summaries.ml
+++ b/lib/transforms/function_summaries.ml
@@ -17,6 +17,8 @@ let append_summary s1 s2 =
 module type FunctionSummaryAnnotation = sig
   val requires : ID.t -> Expr.BasilExpr.t list
   val ensures : ID.t -> Expr.BasilExpr.t list
+  val inout : ID.t -> VarSet.t
+  val id : ID.t
 end
 
 (** Replace gamma expressions with gamma variables for an smt query *)
@@ -76,14 +78,25 @@ let wp_dual_requires (module S : FunctionSummaryAnnotation)
   Analysis.A.M.find_opt Procedure.Vert.Entry result
   |> Option.map Domain.to_pred |> Option.to_list
 
+let sp_ensures (module S : FunctionSummaryAnnotation) (proc : Program.proc) =
+  let module Domain = Sp.Domain (S) in
+  let module Analysis = Intra_analysis.Forwards (Domain) in
+  let result =
+    Analysis.analyse ~widening_set:Graph.ChaoticIteration.FromWto
+      ~widening_delay:5 proc
+  in
+  Analysis.A.M.find_opt Procedure.Vert.Return result
+  |> Option.map Domain.to_pred |> Option.to_list
+
 (** Compute an extension of the given procedure's summary *)
 let extra_summary (solver : Bincaml_util.Smt.Solver.t)
     (module S : FunctionSummaryAnnotation) reiter (proc : Program.proc) =
   (* TODO implement a sample ensures clause generator and some sort of analysis
      pass runner *)
   let cur_req = S.requires (Procedure.id proc) in
+  let cur_ens = S.ensures (Procedure.id proc) in
   if IDSet.mem (Procedure.id proc) !reiter then
-    { requires = cur_req; ensures = [] }
+    { requires = cur_req; ensures = cur_ens }
   else
     let requires =
       wp_dual_requires (module S) proc
@@ -98,7 +111,20 @@ let extra_summary (solver : Bincaml_util.Smt.Solver.t)
                  r :: rs)
            []
     in
-    { requires; ensures = [] }
+    let ensures =
+      sp_ensures (module S) proc
+      |> List.fold_left
+           (fun rs r ->
+             let open Bincaml_util.Smt in
+             match redundant solver r (List.append rs cur_ens) with
+             | Unsat -> rs
+             | Sat -> r :: rs
+             | Unknown ->
+                 reiter := IDSet.add (Procedure.id proc) !reiter;
+                 r :: rs)
+           []
+    in
+    { requires; ensures }
 
 let set_summary summary (proc : Program.proc) =
   let spec = Procedure.specification proc in
@@ -118,6 +144,20 @@ let add_summary summary (proc : Program.proc) =
   in
   Procedure.set_specification proc spec
 
+let add_decls solver prog =
+  Program.declarations prog |> Iter.from_iter |> Iter.map snd
+  |> Iter.filter
+       Program.(
+         function
+         | Type { binding } -> true
+         | Variable { binding } -> Var.is_constant binding
+         | Function { binding } -> Var.is_constant binding
+         | Procedure { definition } -> false)
+  |> Iter.map (fun d -> Expr_smt.SMTLib2.trans_decl d Expr_smt.SMTLib2.empty)
+  |> Iter.map fst
+  |> fun i ->
+  Iter.for_each i (fun s -> Bincaml_util.Smt.Solver.add_command solver s)
+
 let intraproc_transform_proc (prog : Program.t) (proc : Program.proc) =
   let solver =
     Bincaml_util.Smt.Solver.create
@@ -126,20 +166,7 @@ let intraproc_transform_proc (prog : Program.t) (proc : Program.proc) =
         log = Bincaml_util.Smt.Config.quiet_log;
       }
   in
-  let sexps =
-    Program.declarations prog |> Iter.from_iter |> Iter.map snd
-    |> Iter.filter
-         Program.(
-           function
-           | Type { binding } -> true
-           | Variable { binding } -> Var.is_constant binding
-           | Function { binding } -> Var.is_constant binding
-           | Procedure { definition } -> false)
-    |> Iter.map (fun d -> Expr_smt.SMTLib2.trans_decl d Expr_smt.SMTLib2.empty)
-    |> Iter.map fst
-    |> fun i ->
-    Iter.for_each i (fun s -> Bincaml_util.Smt.Solver.add_command solver s)
-  in
+  add_decls solver prog;
   let summary =
     extra_summary solver
       (module struct
@@ -154,6 +181,19 @@ let intraproc_transform_proc (prog : Program.t) (proc : Program.proc) =
           |> Option.map_or
                (fun p -> (Procedure.specification p).ensures)
                ~default:[]
+
+        let inout id =
+          Program.proc_opt prog id
+          |> Option.map_or
+               (fun p ->
+                 VarSet.union
+                   (VarSet.of_iter @@ StringMap.values
+                   @@ Procedure.formal_in_params p)
+                   (VarSet.of_iter @@ StringMap.values
+                   @@ Procedure.formal_out_params p))
+               ~default:VarSet.empty
+
+        let id = Procedure.id proc
       end : FunctionSummaryAnnotation)
       (ref IDSet.empty) proc
   in
@@ -163,7 +203,7 @@ let intraproc_transform_proc (prog : Program.t) (proc : Program.proc) =
 let intraproc_transform (prog : Program.t) =
   let module Dfs = Graph.Traverse.Dfs (Program.CallGraph.G) in
   let cg = Program.CallGraph.make_call_graph prog in
-  Iter.from_iter (fun f -> Dfs.postfix f cg)
+  Iter.from_iter (fun f -> Dfs.prefix f cg)
   |> Iter.fold
        (fun prog v ->
          match v with
@@ -209,12 +249,31 @@ let solve_component (solver : Bincaml_util.Smt.Solver.t) g (prog : Program.t)
 
           let ensures id =
             List.append (IDMap.find id res).ensures (vals id).ensures
+
+          let inout id =
+            Program.proc_opt prog id
+            |> Option.map_or
+                 (fun p ->
+                   VarSet.union
+                     (VarSet.of_iter @@ StringMap.values
+                     @@ Procedure.formal_in_params p)
+                     (VarSet.of_iter @@ StringMap.values
+                     @@ Procedure.formal_out_params p))
+                 ~default:VarSet.empty
+
+          let id = pid
         end : FunctionSummaryAnnotation)
       in
       let extra =
         extra_summary solver annotations reiters (IDMap.find pid procs)
       in
-      append_summary (vals pid) extra
+      if
+        Option.get_or ~default:false
+        @@ Option.map
+             (fun proc -> ID.equal pid (Procedure.id proc))
+             (Program.entry_proc_opt prog)
+      then vals pid (* Makes no sense to generate summary for entrypoint. *)
+      else append_summary (vals pid) extra
     else IDMap.get_or pid res ~default:Domain.bottom
   in
   let sol = FixSummaries.lfp eqs in
@@ -233,6 +292,7 @@ let interproc_transform (prog : Program.t) =
         log = Bincaml_util.Smt.Config.quiet_log;
       }
   in
+  add_decls solver prog;
   let summaries =
     Program.procs prog
     |> Iter.map (fun (i, proc) ->
diff --git a/lib/transforms/may_read_uninit.ml b/lib/transforms/may_read_uninit.ml
index 9785a15a..ccd40f19 100644
--- a/lib/transforms/may_read_uninit.ml
+++ b/lib/transforms/may_read_uninit.ml
@@ -71,7 +71,7 @@ module ReadUninitAnalysis = struct
   let show_short st =
     read_uninit_vars st |> Iter.to_string ~sep:", " Var.to_string
 
-  let init p =
+  let init ?vertex p =
     Procedure.formal_in_params p
     |> Common.StringMap.values
     |> Iter.fold (fun acc v -> update v ReadUninit.Write acc) bottom
diff --git a/lib/transforms/memory_specification.ml b/lib/transforms/memory_specification.ml
index c6ff3e95..ae558c01 100644
--- a/lib/transforms/memory_specification.ml
+++ b/lib/transforms/memory_specification.ml
@@ -5,6 +5,7 @@ open Ops
 open Memory_encoding
 
 let old e = BasilExpr.unexp ~op:`Old e
+let i = Var.create ~scope:Var.LocalConst "i" (Types.Bitvector 64)
 
 let r n =
   BasilExpr.rvar
@@ -31,7 +32,28 @@ let transform_main p =
       spec with
       requires =
         spec.requires
+        (* Require memory is initialized. *)
         @ [ Calls.init_encoding [ BasilExpr.rvar Globals.mem_encoding ] ];
+      (* Ensure there are no memory leaks. *)
+      ensures =
+        spec.ensures
+        @ [
+            BasilExpr.forall ~bound:[ i ]
+            @@ BasilExpr.binexp ~op:`IMPLIES
+                 (Calls.addr_is_heap
+                    [ BasilExpr.rvar Globals.mem_encoding; BasilExpr.rvar i ])
+                 (BasilExpr.binexp ~op:`NEQ
+                    (Calls.alloc_live
+                       [
+                         BasilExpr.rvar Globals.mem_encoding;
+                         Calls.addr_alloc
+                           [
+                             BasilExpr.rvar Globals.mem_encoding;
+                             BasilExpr.rvar i;
+                           ];
+                       ])
+                    (BasilExpr.bvconst live));
+          ];
       modifies_globs = spec.modifies_globs @ [ Globals.mem_encoding ];
       captures_globs = spec.captures_globs @ [ Globals.mem_encoding ];
     }
@@ -139,15 +161,17 @@ let transform_proc entry _ (p : Program.proc) =
       p
   in
   let name = ID.name (Procedure.id p) in
-  match name with
-  | "@main" -> transform_main p
-  | e when String.equal entry e -> transform_main p
-  | "@malloc" -> transform_malloc p
-  | "@free" -> transform_free p
-  | "@#malloc" -> transform_malloc p
-  | "@zmalloc" -> transform_malloc p
-  | "@#free" -> transform_free p
-  | _ -> p
+  if Procedure.attrib p |> StringMap.mem ".entrypoint" then transform_main p
+  else
+    match name with
+    | "@main" -> transform_main p
+    | e when String.equal entry e -> transform_main p
+    | "@malloc" -> transform_malloc p
+    | "@free" -> transform_free p
+    | "@#malloc" -> transform_malloc p
+    | "@zmalloc" -> transform_malloc p
+    | "@#free" -> transform_free p
+    | _ -> p
 
 let transform (p : Program.t) =
   let entry = Program.entry_proc_exn p |> Procedure.id %> ID.name in
diff --git a/lib/transforms/ssa.ml b/lib/transforms/ssa.ml
index 1c085828..4af27a0b 100644
--- a/lib/transforms/ssa.ml
+++ b/lib/transforms/ssa.ml
@@ -255,10 +255,12 @@ let lift_procedure_params prog ~skip_observable ~skip_maps all_lifted procid
     (* Rewrite ensures: Old(g) → g_in (entry value); bare modified g →
            g_out (exit value); bare captured-only g → g_in (unchanged).
            Old(g) is handled first so the bare-g pass doesn't clobber it. *)
+    let fvs = Expr.BasilExpr.free_vars expr in
     let alg node =
       match node with
       | UnaryExpr { op = `Old; arg } -> replace [%here] (rewrite_old_expr arg)
-      | RVar { id } when Var.is_constant id -> Keep
+      | RVar { id } when Var.is_constant id || (not @@ VarSet.mem id fvs) ->
+          Keep
       | RVar { id } -> (
           match StringMap.find_opt (Var.name id) glob_to_outparam with
           | Some v -> replace [%here] (rvar v)
diff --git a/nix/shell.nix b/nix/shell.nix
index 87c1501d..7701f368 100644
--- a/nix/shell.nix
+++ b/nix/shell.nix
@@ -18,6 +18,14 @@
   bnfc-treesitter,
   boogie,
   cvc5,
+  linol-lwt,
+  linol,
+
+  # lsp
+  ppx_import,
+  logs,
+  mtime,
+  z3,
 }:
 
 mkShell {
@@ -32,6 +40,12 @@ mkShell {
     boogie
     cvc5
     bincaml_lsp
+    linol
+    linol-lwt
+    ppx_import
+    logs
+    mtime
+    z3.out
     # sherlodoc - not in nixpkgs?
   ]
   ++ lib.optional stdenv.hostPlatform.isLinux perf;
diff --git a/test/cram/dune b/test/cram/dune
index d27e91d9..eb12ff8b 100644
--- a/test/cram/dune
+++ b/test/cram/dune
@@ -9,7 +9,7 @@
   concat.il))
 
 (cram
- (applies_to * \ expr_smt malloc_free)
+ (applies_to * \ expr_smt malloc_free memory_safety memory_interproc)
  (package bincaml)
  (deps
   loop_dfg.sexp
@@ -46,7 +46,7 @@
   ../../bin/main.exe))
 
 (cram
- (applies_to malloc_free)
+ (applies_to malloc_free memory_safety memory_interproc)
  (package bincaml)
  (enabled_if
   (and %{bin-available:boogie} %{bin-available:cvc5}))
@@ -54,4 +54,8 @@
   %{bin:bincaml}
   ../../examples/memory/malloc_free.il
   ../../examples/memory/malloc_free_oob.il
-  ./malloc_free.sexp))
+  ./malloc_free.sexp
+  ../../examples/memory/memory_interproc.il
+  ./memory_interproc.sexp
+  ../../examples/memory/memory_safety.il
+  ./memory_safety.sexp))
diff --git a/test/cram/malloc_free.t b/test/cram/malloc_free.t
index 36b6a764..91861b54 100644
--- a/test/cram/malloc_free.t
+++ b/test/cram/malloc_free.t
@@ -133,6 +133,13 @@
      R29_in: bv64, R30_in: bv64, R31_in: bv64, _PC_in: bv64) returns (R0_out: bv64,
      R17_out: bv64, R1_out: bv64, R29_out: bv64, R30_out: bv64);
     modifies $mem_encoding, $mem, $stack;
+    ensures (forall 
+     i: bv64 :: 
+      
+     ($me_addr_is_heap($mem_encoding, i) ==> ($me_alloc_live(
+         $mem_encoding,
+         $me_addr_alloc($mem_encoding, i)
+       ) != 1bv2)));
     requires $me_init_encoding($mem_encoding);
   implementation p$main_2276(R0_in: bv64, R16_in: bv64, R17_in: bv64, R1_in: bv64,
    R29_in: bv64, R30_in: bv64, R31_in: bv64, _PC_in: bv64) returns (R0_out: bv64,
@@ -342,6 +349,13 @@
      R29_in: bv64, R30_in: bv64, R31_in: bv64, _PC_in: bv64) returns (R0_out: bv64,
      R17_out: bv64, R1_out: bv64, R29_out: bv64, R30_out: bv64);
     modifies $mem_encoding, $mem, $stack;
+    ensures (forall 
+     i: bv64 :: 
+      
+     ($me_addr_is_heap($mem_encoding, i) ==> ($me_alloc_live(
+         $mem_encoding,
+         $me_addr_alloc($mem_encoding, i)
+       ) != 1bv2)));
     requires $me_init_encoding($mem_encoding);
   implementation p$main_2276(R0_in: bv64, R16_in: bv64, R17_in: bv64, R1_in: bv64,
    R29_in: bv64, R30_in: bv64, R31_in: bv64, _PC_in: bv64) returns (R0_out: bv64,
@@ -427,8 +441,8 @@
     requires ($me_alloc_live($mem_encoding, $me_addr_alloc($mem_encoding, R0_in)) == 1bv2);
 
   $ boogie ./bad.bpl
-  ./bad.bpl(162,5): Error: this assertion could not be proved
+  ./bad.bpl(169,5): Error: this assertion could not be proved
   Execution trace:
-      ./bad.bpl(136,3): b#main_entry
+      ./bad.bpl(143,3): b#main_entry
   
   Boogie program verifier finished with 0 verified, 1 error
diff --git a/test/cram/memory_interproc.sexp b/test/cram/memory_interproc.sexp
new file mode 100644
index 00000000..6ba88af0
--- /dev/null
+++ b/test/cram/memory_interproc.sexp
@@ -0,0 +1,16 @@
+(load-il "../../examples/memory/memory_interproc.il")
+
+(run-transforms "ssa")
+
+(run-transforms "split-memory-encoding")
+(run-transforms "memory-specification")
+
+(run-transforms "ssa")
+
+(run-transforms "linear-const")
+(run-transforms "linear-copy")
+
+(run-transforms "inter-function-summaries")
+
+(dump-il "after.il")
+(dump-boogie "out.bpl")
diff --git a/test/cram/memory_interproc.t b/test/cram/memory_interproc.t
new file mode 100644
index 00000000..ee8b5e74
--- /dev/null
+++ b/test/cram/memory_interproc.t
@@ -0,0 +1,14 @@
+  $ bincaml script memory_interproc.sexp
+  (load-il ../../examples/memory/memory_interproc.il)
+  (run-transforms ssa)
+  (run-transforms split-memory-encoding)
+  (run-transforms memory-specification)
+  (run-transforms ssa)
+  (run-transforms linear-const)
+  (run-transforms linear-copy)
+  (run-transforms inter-function-summaries)
+  (dump-il after.il)
+  (dump-boogie out.bpl)
+  $ boogie out.bpl
+  
+  Boogie program verifier finished with 2 verified, 0 errors
diff --git a/test/cram/memory_safety.sexp b/test/cram/memory_safety.sexp
new file mode 100644
index 00000000..01ac843a
--- /dev/null
+++ b/test/cram/memory_safety.sexp
@@ -0,0 +1,14 @@
+(load-il "../../examples/memory/memory_safety.il")
+
+(run-transforms "ssa")
+
+(run-transforms "split-memory-encoding")
+(run-transforms "memory-specification")
+
+(run-transforms "ssa")
+
+(run-transforms "linear-const")
+(run-transforms "linear-copy")
+
+(dump-il "after.il")
+(dump-boogie "out.bpl")
diff --git a/test/cram/memory_safety.t b/test/cram/memory_safety.t
new file mode 100644
index 00000000..9ae58fb6
--- /dev/null
+++ b/test/cram/memory_safety.t
@@ -0,0 +1,31 @@
+  $ bincaml script memory_safety.sexp
+  (load-il ../../examples/memory/memory_safety.il)
+  (run-transforms ssa)
+  (run-transforms split-memory-encoding)
+  (run-transforms memory-specification)
+  (run-transforms ssa)
+  (run-transforms linear-const)
+  (run-transforms linear-copy)
+  (dump-il after.il)
+  (dump-boogie out.bpl)
+  $ boogie out.bpl
+  out.bpl(193,5): Error: a precondition for this call could not be proved
+  out.bpl(112,3): Related location: this is the precondition that could not be proved
+  Execution trace:
+      out.bpl(180,3): b#inputs
+  out.bpl(224,5): Error: a precondition for this call could not be proved
+  out.bpl(111,3): Related location: this is the precondition that could not be proved
+  Execution trace:
+      out.bpl(218,3): b#inputs
+  out.bpl(265,5): Error: this assertion could not be proved
+  Execution trace:
+      out.bpl(254,3): b#inputs
+  out.bpl(303,5): Error: this assertion could not be proved
+  Execution trace:
+      out.bpl(296,3): b#inputs
+  out.bpl(355,5): Error: a postcondition could not be proved on this return path
+  out.bpl(319,3): Related location: this is the postcondition that could not be proved
+  Execution trace:
+      out.bpl(337,3): b#inputs
+  
+  Boogie program verifier finished with 1 verified, 5 errors