diff --git a/heapster-saw/examples/Makefile b/heapster-saw/examples/Makefile
index 2e554556bb..5bc17e237f 100644
--- a/heapster-saw/examples/Makefile
+++ b/heapster-saw/examples/Makefile
@@ -52,3 +52,6 @@ rust_lifetimes.bc: rust_lifetimes.rs
 
 rust_lifetimes.v: rust_lifetimes.bc rust_lifetimes.saw
 	$(SAW) rust_lifetimes.saw
+
+clearbufs.v: clearbufs.bc clearbufs.saw clearbufs.sawcore
+	$(SAW) clearbufs.saw
diff --git a/heapster-saw/examples/_CoqProject b/heapster-saw/examples/_CoqProject
index e1e979ae60..206c114432 100644
--- a/heapster-saw/examples/_CoqProject
+++ b/heapster-saw/examples/_CoqProject
@@ -23,3 +23,5 @@ rust_data_proofs.v
 rust_lifetimes.v
 rust_lifetimes_proofs.v
 arrays.v
+clearbufs.v
+clearbufs_proofs.v
diff --git a/heapster-saw/examples/clearbufs.bc b/heapster-saw/examples/clearbufs.bc
new file mode 100644
index 0000000000..7484039808
Binary files /dev/null and b/heapster-saw/examples/clearbufs.bc differ
diff --git a/heapster-saw/examples/clearbufs.c b/heapster-saw/examples/clearbufs.c
new file mode 100644
index 0000000000..3002b50b35
--- /dev/null
+++ b/heapster-saw/examples/clearbufs.c
@@ -0,0 +1,32 @@
+#include <stdlib.h>
+#include <stdint.h>
+
+typedef struct bufs {
+  struct bufs * next;
+  int64_t len;
+  int64_t data [];
+} bufs;
+
+void clearbufs (bufs * lst)
+{
+  // NOTE: the input value of lst is stored in a stack-allocated variable, which
+  // is also called lst below, but is called lp in the paper. This is sort-of
+  // like the following code, except that the following would actually make a
+  // second stack slot for variable lp, unlike the paper example.
+  //
+  // bufs **lp = alloca(8)
+  // *lp = lst;
+
+  while (1) {
+    // NOTE: reading lst here and testing for NULL 
+    //
+    // bufs *l = lst = *lp
+    // if (l == NULL) { ... }
+    if (lst == NULL) {
+      return;
+    } else {
+      lst->data[0] = 0;
+      lst = lst->next;
+    }
+  }
+}
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;
+-}
diff --git a/heapster-saw/examples/clearbufs.v b/heapster-saw/examples/clearbufs.v
new file mode 100644
index 0000000000..bef550c5d7
--- /dev/null
+++ b/heapster-saw/examples/clearbufs.v
@@ -0,0 +1,160 @@
+
+(** Mandatory imports from saw-core-coq *)
+From Coq Require Import Lists.List.
+From Coq Require Import String.
+From Coq Require Import Vectors.Vector.
+From CryptolToCoq Require Import SAWCoreScaffolding.
+From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.
+Import ListNotations.
+
+(** Post-preamble section specified by you *)
+From CryptolToCoq Require Import SAWCorePrelude.
+
+(** Code generated by saw-core-coq *)
+
+Module clearbufs.
+
+Definition BV64 : Type :=
+  @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit).
+
+Definition V64 : Type :=
+  @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool).
+
+Definition bv64_16 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) :=
+  intToBv 64 0x10%Z.
+
+Inductive Mbox : Type :=
+| Mbox_nil : @Mbox
+| Mbox_cons : @Mbox -> forall (len : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)), @SAWCorePrelude.BVVec 64 len BV64 -> @Mbox
+.
+
+Definition Mbox_def : Type :=
+  @Mbox.
+
+Axiom unfoldMbox : @Mbox -> @SAWCorePrelude.Either unit (@sigT V64 (fun (len : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod (@Mbox) (prod (@SAWCorePrelude.BVVec 64 len BV64) unit))) .
+
+Axiom foldMbox : @SAWCorePrelude.Either unit (@sigT V64 (fun (len : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod (@Mbox) (prod (@SAWCorePrelude.BVVec 64 len BV64) unit))) -> @Mbox .
+
+Axiom transMbox : @Mbox -> @Mbox -> @Mbox .
+
+Definition foldBufs : forall (p0 : @SAWCorePrelude.Either unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit)))), Mbox_def :=
+  @foldMbox.
+
+Definition unfoldBufs : forall (p0 : Mbox_def), let var__0   := @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) in
+  @SAWCorePrelude.Either unit (@sigT var__0 (fun (x_ex0 : var__0) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT var__0 (fun (x_ex1 : var__0) => unit))) unit))) :=
+  @unfoldMbox.
+
+Definition transBufs : forall (p0 : Mbox_def), forall (p1 : Mbox_def), Mbox_def :=
+  @transMbox.
+
+Definition clearbufs__tuple_fun : @CompM.lrtTupleType (@CompM.LRT_Cons (@CompM.LRT_Fun Mbox_def (fun (perm0 : Mbox_def) => @CompM.LRT_Ret Mbox_def)) (@CompM.LRT_Nil)) :=
+  @CompM.multiFixM (@CompM.LRT_Cons (@CompM.LRT_Fun Mbox_def (fun (perm0 : Mbox_def) => @CompM.LRT_Ret Mbox_def)) (@CompM.LRT_Nil)) (fun (clearbufs : @CompM.lrtToType (@CompM.LRT_Fun Mbox_def (fun (perm0 : Mbox_def) => @CompM.LRT_Ret Mbox_def))) => pair (fun (p0 : Mbox_def) => @CompM.letRecM (@CompM.LRT_Cons (@CompM.LRT_Fun Mbox_def (fun (p1 : Mbox_def) => @CompM.LRT_Fun Mbox_def (fun (p2 : Mbox_def) => @CompM.LRT_Ret Mbox_def))) (@CompM.LRT_Nil)) Mbox_def (fun (f : @CompM.lrtToType (@CompM.LRT_Fun Mbox_def (fun (p1 : Mbox_def) => @CompM.LRT_Fun Mbox_def (fun (p2 : Mbox_def) => @CompM.LRT_Ret Mbox_def)))) => pair (fun (p1 : Mbox_def) (p2 : Mbox_def) => @SAWCorePrelude.either unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) (CompM Mbox_def) (fun (x_left0 : unit) => (fun (catchpoint : CompM Mbox_def) => @SAWCorePrelude.either unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) (CompM Mbox_def) (fun (x_left1 : unit) => @returnM CompM _ Mbox_def (@foldBufs (@SAWCorePrelude.Left unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) tt))) (fun (x_right0 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) => catchpoint) (@unfoldBufs p1)) (@returnM CompM _ Mbox_def (@transBufs p1 (@foldBufs (@SAWCorePrelude.Left unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) tt))))) (fun (x_right0 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) => @SAWCorePrelude.maybe (@SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreVectorsAsCoqVectors.bvult 64 (intToBv 64 0%Z) (@projT1 (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_elimEx0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_elimEx0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit)) x_right0)) (@SAWCoreScaffolding.true)) (CompM Mbox_def) (@errorM CompM _ Mbox_def "0 <u ghost5"%string) (fun (ult_pf0 : @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreVectorsAsCoqVectors.bvult 64 (intToBv 64 0%Z) (@projT1 (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_elimEx0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_elimEx0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit)) x_right0)) (@SAWCoreScaffolding.true)) => (fun (catchpoint : CompM Mbox_def) => (fun (catchpoint1 : CompM Mbox_def) => @SAWCorePrelude.either unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) (CompM Mbox_def) (fun (x_left0 : unit) => f (@transBufs p1 (@foldBufs (@SAWCorePrelude.Right unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) (@existT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit)) (@projT1 (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_elimEx0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_elimEx0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit)) x_right0) (pair (@foldBufs (@SAWCorePrelude.Left unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) tt)) (pair (@SAWCorePrelude.adjustBVVec 64 (@projT1 (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_elimEx0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_elimEx0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit)) x_right0) (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (SAWCoreScaffolding.fst (SAWCoreScaffolding.snd (@projT2 (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_elimEx0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_elimEx0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit)) x_right0))) (fun (fld0 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) => @existT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit) (intToBv 64 0%Z) tt) (intToBv 64 0%Z)) tt)))))) (@foldBufs (@SAWCorePrelude.Left unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) tt))) (fun (x_right1 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) => catchpoint1) (@unfoldBufs (SAWCoreScaffolding.fst (@projT2 (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_elimEx0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_elimEx0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit)) x_right0)))) (f (@transBufs p1 (@foldBufs (@SAWCorePrelude.Right unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) (@existT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit)) (@projT1 (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_elimEx0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_elimEx0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit)) x_right0) (pair (@foldBufs (@SAWCorePrelude.Left unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) tt)) (pair (@SAWCorePrelude.adjustBVVec 64 (@projT1 (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_elimEx0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_elimEx0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit)) x_right0) (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (SAWCoreScaffolding.fst (SAWCoreScaffolding.snd (@projT2 (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_elimEx0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_elimEx0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit)) x_right0))) (fun (fld0 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) => @existT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit) (intToBv 64 0%Z) tt) (intToBv 64 0%Z)) tt)))))) (@transBufs (SAWCoreScaffolding.fst (@projT2 (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_elimEx0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_elimEx0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit)) x_right0)) (@foldBufs (@SAWCorePrelude.Left unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) tt))))) (@SAWCorePrelude.either unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) (CompM Mbox_def) (fun (x_left0 : unit) => f (@transBufs p1 (@foldBufs (@SAWCorePrelude.Right unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) (@existT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit)) (@projT1 (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_elimEx0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_elimEx0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit)) x_right0) (pair (@transBufs (SAWCoreScaffolding.fst (@projT2 (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_elimEx0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_elimEx0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit)) x_right0)) (@foldBufs (@SAWCorePrelude.Left unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) tt))) (pair (@SAWCorePrelude.adjustBVVec 64 (@projT1 (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_elimEx0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_elimEx0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit)) x_right0) (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (SAWCoreScaffolding.fst (SAWCoreScaffolding.snd (@projT2 (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_elimEx0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_elimEx0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit)) x_right0))) (fun (fld0 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) => @existT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit) (intToBv 64 0%Z) tt) (intToBv 64 0%Z)) tt)))))) (@foldBufs (@SAWCorePrelude.Left unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) tt))) (fun (x_right1 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) => @errorM CompM _ Mbox_def "
+  Could not prove
+    (z9, z8).
+      top1:Bufs<z8>, local2:ptr((W,0) |-> eq(z8)),
+      z9:llvmframe [local2:8], z8:Bufs<LLVMword 0>
+
+  proveEq: Could not prove ghost4 = (z9, z8). LLVMword 0
+
+  --------------------
+
+  proveEq: Could not prove ghost4 = (z10, z9). ghost7
+
+  --------------------
+
+  proveEq: Could not prove top1 = (z10, z9). LLVMword 0
+
+  --------------------
+
+  proveEq: Could not prove top1 = (z11, z10). ghost7
+
+  --------------------
+
+  proveEq: Could not prove ghost4 = (z9, z8). LLVMword 0
+
+  --------------------
+
+  proveEq: Could not prove ghost4 = (z10, z9). ghost7
+
+  --------------------
+
+  proveEq: Could not prove ghost7 = (z14, z13). LLVMword 0
+
+  --------------------
+
+  proveVarImplH: Could not prove
+  z12:eq(LLVMword 0)
+  -o
+  (z15, z14, z13).
+    ptr((W,0) |-> Bufs<LLVMword 0>)
+      *ptr((W,8) |-> eq(LLVMword z13))
+      *array(16, <z13, *8, [(W,0) |-> int64<>], [])
+
+  --------------------
+
+  proveVarImplH: Could not prove
+  ghost7:eq(LLVMword 0)
+  -o
+  (z15, z14, z13).
+    ptr((W,0) |-> Bufs<LLVMword 0>)
+      *ptr((W,8) |-> eq(LLVMword z13))
+      *array(16, <z13, *8, [(W,0) |-> int64<>], [])
+
+  --------------------
+
+  proveEq: Could not prove LLVMword 0 = (z12, z11, z10). ghost7
+
+  --------------------
+
+  proveVarImplH: Could not prove
+  z8:eq(LLVMword 0)
+  -o
+  (z12, z11, z10, z9).
+    ptr((W,0) |-> Bufs<z11>)
+      *ptr((W,8) |-> eq(LLVMword z9))
+      *array(16, <z9, *8, [(W,0) |-> int64<>], [])"%string) (@unfoldBufs (SAWCoreScaffolding.fst (@projT2 (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_elimEx0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_elimEx0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit)) x_right0))))) (@SAWCorePrelude.bvultWithProof 64 (intToBv 64 0%Z) (@projT1 (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_elimEx0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_elimEx0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit)) x_right0))) (@unfoldBufs p2)) tt) (fun (f : @CompM.lrtToType (@CompM.LRT_Fun Mbox_def (fun (p1 : Mbox_def) => @CompM.LRT_Fun Mbox_def (fun (p2 : Mbox_def) => @CompM.LRT_Ret Mbox_def)))) => (fun (catchpoint : CompM Mbox_def) => (fun (catchpoint1 : CompM Mbox_def) => @SAWCorePrelude.either unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) (CompM Mbox_def) (fun (x_left0 : unit) => f (@foldBufs (@SAWCorePrelude.Left unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) tt)) (@foldBufs (@SAWCorePrelude.Left unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) tt))) (fun (x_right0 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) => catchpoint1) (@unfoldBufs p0)) (f (@foldBufs (@SAWCorePrelude.Left unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) tt)) (@transBufs p0 (@foldBufs (@SAWCorePrelude.Left unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) tt))))) (@SAWCorePrelude.either unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) (CompM Mbox_def) (fun (x_left0 : unit) => f (@transBufs p0 (@foldBufs (@SAWCorePrelude.Left unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) tt))) (@foldBufs (@SAWCorePrelude.Left unit (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) tt))) (fun (x_right0 : @sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex0 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => prod Mbox_def (prod (@SAWCorePrelude.BVVec 64 x_ex0 (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (x_ex1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit))) unit))) => @errorM CompM _ Mbox_def "
+  Could not prove
+    (z6, z5).
+      top1:Bufs<z5>, local2:ptr((W,0) |-> eq(z5)),
+      z6:llvmframe [local2:8], z5:Bufs<LLVMword 0>
+
+  proveEq: Could not prove top1 = (z9, z8). LLVMword 0
+
+  --------------------
+
+  proveVarImplH: Could not prove
+  z7:eq(LLVMword 0)
+  -o
+  (z10, z9, z8).
+    ptr((W,0) |-> Bufs<LLVMword 0>)
+      *ptr((W,8) |-> eq(LLVMword z8))
+      *array(16, <z8, *8, [(W,0) |-> int64<>], [])
+
+  --------------------
+
+  proveVarImplH: Could not prove
+  top1:eq(LLVMword 0)
+  -o
+  (z10, z9, z8).
+    ptr((W,0) |-> Bufs<LLVMword 0>)
+      *ptr((W,8) |-> eq(LLVMword z8))
+      *array(16, <z8, *8, [(W,0) |-> int64<>], [])
+
+  --------------------
+
+  proveEq: Could not prove LLVMword 0 = (z8, z7). top1
+
+  --------------------
+
+  proveVarImplH: Could not prove
+  z5:eq(LLVMword 0)
+  -o
+  (z8, z7, z6).
+    ptr((W,0) |-> Bufs<z7>)
+      *ptr((W,8) |-> eq(LLVMword z6))
+      *array(16, <z6, *8, [(W,0) |-> int64<>], [])"%string) (@unfoldBufs p0)))) tt).
+
+Definition clearbufs : @CompM.lrtToType (@CompM.LRT_Fun Mbox_def (fun (perm0 : Mbox_def) => @CompM.LRT_Ret Mbox_def)) :=
+  SAWCoreScaffolding.fst clearbufs__tuple_fun.
+
+End clearbufs.
diff --git a/heapster-saw/examples/clearbufs_proofs.v b/heapster-saw/examples/clearbufs_proofs.v
new file mode 100644
index 0000000000..8f097be88a
--- /dev/null
+++ b/heapster-saw/examples/clearbufs_proofs.v
@@ -0,0 +1,14 @@
+From Coq          Require Import Lists.List.
+From Coq          Require Import String.
+From Coq          Require Import Vectors.Vector.
+From CryptolToCoq Require Import SAWCoreScaffolding.
+From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.
+From CryptolToCoq Require Import SAWCoreBitvectors.
+
+From CryptolToCoq Require Import SAWCorePrelude.
+From CryptolToCoq Require Import CompMExtra.
+
+Require Import Examples.clearbufs.
+Import clearbufs.
+
+(* Eval cbn in clearbufs__tuple_fun. *)
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
index 2fb48c7dbf..457aa272bb 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
@@ -5865,8 +5865,13 @@ proveVarAtomicImpl x ps mb_p = case mbMatch mb_p of
     partialSubstForceM (fmap llvmFieldOffset mb_fp) "proveVarPtrPerms" >>>= \off ->
     foldMapWithDefault implCatchM
     (proveVarAtomicImplUnfoldOrFail x ps mb_p)
-    (\(i,_) -> proveVarLLVMField x ps i off mb_fp)
-    (findMaybeIndices (llvmPermContainsOffset off) ps)
+    (\(i,_) -> proveVarLLVMField x ps i off mb_fp) $
+    -- If there are any permissions that definitely contain off, use those, and
+    -- otherwise iterate through all those that could contain off
+    let ixs_props = findMaybeIndices (llvmPermContainsOffset off) ps in
+    case filter (\(_,props) -> all bvPropHolds props) ixs_props of
+      [] -> ixs_props
+      ixs_props_hold -> ixs_props_hold
 
   [nuMP| Perm_LLVMArray mb_ap |] ->
     partialSubstForceM mb_ap "proveVarPtrPerms" >>>= \ap ->