diff --git a/heapster-saw/examples/clearbufs.saw b/heapster-saw/examples/clearbufs.saw
new file mode 100644
index 0000000000..689934b9a6
--- /dev/null
+++ b/heapster-saw/examples/clearbufs.saw
@@ -0,0 +1,13 @@
+enable_experimental;
+env <- heapster_init_env_from_file "clearbufs.sawcore" "clearbufs.bc";
+
+// Integer types
+heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
+
+heapster_define_reachability_perm env "Bufs" "x:llvmptr 64" "llvmptr 64" "exists len:(bv 64).ptr((W,0) |-> Bufs<x>) * ptr((W,8) |-> eq(llvmword(len))) * array(16, <len, *8, [(W,0) |-> int64<>])" "Mbox_def" "foldMbox" "unfoldMbox" "transMbox";
+
+heapster_block_entry_hint env "clearbufs" 3 "top1:llvmptr 64" "frm:llvmframe 64,ghost:llvmptr 64" "top1:Bufs<ghost>, arg0:ptr((W,0) |-> eq(ghost)), ghost:Bufs<llvmword(0)>,frm:llvmframe [arg0:8]";
+
+heapster_typecheck_fun env "clearbufs" "().arg0:Bufs<llvmword(0)> -o arg0:Bufs<llvmword(0)>";
+
+heapster_export_coq env "clearbufs.v";
diff --git a/heapster-saw/examples/clearbufs.sawcore b/heapster-saw/examples/clearbufs.sawcore
new file mode 100644
index 0000000000..c5862e0dcc
--- /dev/null
+++ b/heapster-saw/examples/clearbufs.sawcore
@@ -0,0 +1,63 @@
+
+module clearbufs where
+
+import Prelude;
+
+BV64 : sort 0;
+BV64 = Sigma (Vec 64 Bool) (\ (_:Vec 64 Bool) -> #());
+
+V64 : sort 0;
+V64 = Vec 64 Bool;
+
+-- Harcoded 64 length bitvector value 16, used for mbox definitions
+bv64_16 : Vec 64 Bool;
+bv64_16 = [False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,True,False,False,False,False];
+
+data Mbox : sort 0 where {
+  Mbox_nil : Mbox;
+  Mbox_cons : Mbox -> (len : Vec 64 Bool) -> BVVec 64 len BV64 -> Mbox;
+}
+
+-- A definition for the Mbox datatype; currently needed as a workaround in Heapster
+Mbox_def : sort 0;
+Mbox_def = Mbox;
+
+{- Mbox__rec : (P : Mbox -> sort 0) ->
+            (P Mbox_nil) ->
+            ((m:Mbox) -> P m -> (len:BV64) -> (d:BVVec 64 bv64_16 BV64) -> P (Mbox_cons m len d)) ->
+            (m:Mbox) -> P m;
+Mbox__rec P f1 f2 m = Mbox#rec P f1 f2 m; -}
+
+--unfoldMbox : Mbox -> Either #() (Mbox * BV64 * BVVec 64 bv64_16 BV64 * #());
+primitive
+unfoldMbox : Mbox -> Either #() (Sigma (V64) (\ (len : V64) -> Mbox * BVVec 64 len BV64 * #()));
+
+{-unfoldMbox m =
+  Mbox__rec (\ (_:Mbox) -> Either #() (Mbox * BV64 * BVVec 64 bv64_16 BV64 * #()))
+  (Left #() (Mbox * BV64 * BVVec 64 bv64_16 BV64 * #()) ())
+  (\ (m:Mbox) (_:Either #() (Mbox * BV64 * BVVec 64 bv64_16 BV64 * #())) (len:BV64) (d:BVVec 64 bv64_16 BV64) ->
+     Right #() (Mbox * BV64 * BVVec 64 bv64_16 BV64 * #()) (m, len, d, ()))
+  m;
+  -}
+
+primitive
+foldMbox : Either #() (Sigma (V64) (\ (len : V64) -> Mbox * BVVec 64 len BV64 * #())) -> Mbox;
+
+--(Mbox * BV64 * (BVVec 64 bv64_16 BV64) * #()) -> Mbox;
+{-
+foldMbox =
+  either #() (Mbox * BV64 * (BVVec 64 bv64_16 BV64) * #()) Mbox
+         (\ (_:#()) -> Mbox_nil)
+         (\ (tup : (Mbox * BV64 * (BVVec 64 bv64_16 BV64) * #())) ->
+            Mbox_cons tup.1 tup.2 tup.3);
+			-}
+
+primitive
+transMbox : Mbox -> Mbox -> Mbox;
+{-
+transMbox m1 m2 =
+  Mbox__rec (\ (_ : Mbox) -> Mbox)
+  m2
+  (\ (_ : Mbox) (rec:Mbox) (len : BV64) (vec : BVVec 64 bv64_16 BV64) -> Mbox_cons rec len vec)
+  m1;
+-}