diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml
index 7f9a35f80..7384a1a63 100644
--- a/sledge/src/symbheap/solver.ml
+++ b/sledge/src/symbheap/solver.ml
@@ -606,6 +606,7 @@ let excise_dnf : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option =
           let ws, sub = Sh.bind_exists sub ~wrt:xs in
           let sub = Sh.and_cong min.cong sub in
           let zs = Var.Set.empty in
+          let min = Sh.extend_us ws min in
           excise {us; com; min; xs; sub; zs; pgs= true}
           >>| fun remainder -> Sh.exists (Set.union ys ws) remainder )
       >>| fun remainder -> Sh.or_ remainders remainder )
diff --git a/sledge/src/symbheap/solver_test.ml b/sledge/src/symbheap/solver_test.ml
index 21a0a3f79..e68c71260 100644
--- a/sledge/src/symbheap/solver_test.ml
+++ b/sledge/src/symbheap/solver_test.ml
@@ -88,6 +88,25 @@ let%test_module _ =
           \-   %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩
         ) infer_frame:   emp |}]
 
+    let%expect_test _ =
+      let common = Sh.seg {loc= l2; bas= b; len= !10; siz= !10; arr= a2} in
+      let seg1 = Sh.seg {loc= l; bas= b; len= !10; siz= !10; arr= a} in
+      let minued = Sh.star common seg1 in
+      let subtrahend =
+        Sh.and_ (Exp.eq m n)
+          (Sh.exists
+             (Var.Set.of_list [m_])
+             (Sh.extend_us (Var.Set.of_list [m_]) common))
+      in
+      infer_frame minued [n_; m_] subtrahend ;
+      [%expect
+        {|
+        ( infer_frame:
+            %l_6 -[ %b_4, 10 )-> ⟨10,%a_1⟩ * %l_7 -[ %b_4, 10 )-> ⟨10,%a_2⟩
+          \- ∃ %m_8, %n_9 .
+            ∃ %m_10 .   %m_8 = %n_9 ∧ %l_7 -[ %b_4, 10 )-> ⟨10,%a_2⟩
+        ) infer_frame: ∃ %m_10 .   %l_6 -[ %b_4, 10 )-> ⟨10,%a_1⟩ |}]
+
     let%expect_test _ =
       check_frame
         (Sh.star