diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index 3f9f0d9d3..3b1e990d1 100644
--- a/sledge/src/llair/exp.ml
+++ b/sledge/src/llair/exp.ml
@@ -894,8 +894,6 @@ let rec simp_not (typ : Typ.t) exp =
       simp_cond cnd (simp_not typ thn) (simp_not typ els)
   (* ¬false ==> true ¬true ==> false *)
   | Integer {data}, Integer {bits= 1} -> bool (Z.is_false data)
-  (* ¬b ==> false = b *)
-  | b, Integer {bits= 1} -> App {op= App {op= Eq; arg= bool false}; arg= b}
   (* ¬e ==> true xor e *)
   | e, _ ->
       App {op= App {op= Xor; arg= integer (Z.of_bool true) typ}; arg= e}
@@ -938,11 +936,6 @@ let simp_xor x y =
   | Integer {data= i; typ}, Integer {data= j} ->
       let bits = Option.value_exn (Typ.prim_bit_size_of typ) in
       integer (Z.blogxor ~bits i j) typ
-  (* true xor b ==> ¬b *)
-  | Integer {data; typ= Integer {bits= 1}}, b
-   |b, Integer {data; typ= Integer {bits= 1}}
-    when Z.is_true data ->
-      simp_not Typ.bool b
   | _ -> App {op= App {op= Xor; arg= x}; arg= y}
 
 let simp_shl x y =
diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml
index 5ee90ae70..63c2b0416 100644
--- a/sledge/src/symbheap/sh.ml
+++ b/sledge/src/symbheap/sh.ml
@@ -380,9 +380,20 @@ let rec pure (e : Term.t) =
   [%Trace.call fun {pf} -> pf "%a" Term.pp e]
   ;
   let us = Term.fv e in
+  let eq_false b =
+    let cong = Equality.and_eq b (Term.bool false) Equality.true_ in
+    {emp with us; cong; pure= [e]}
+  in
   ( match e with
   | Integer {data; typ= Integer {bits= 1}} ->
       if Z.is_false data then false_ us else emp
+  (* ¬b ==> false = b *)
+  | App {op= App {op= Xor; arg= Integer {data; typ= Integer {bits= 1}}}; arg}
+    when Z.is_true data ->
+      eq_false arg
+  | App {op= App {op= Xor; arg}; arg= Integer {data; typ= Integer {bits= 1}}}
+    when Z.is_true data ->
+      eq_false arg
   | App {op= App {op= And; arg= e1}; arg= e2} -> star (pure e1) (pure e2)
   | App {op= App {op= Or; arg= e1}; arg= e2} -> or_ (pure e1) (pure e2)
   | App {op= App {op= App {op= Conditional; arg= cnd}; arg= thn}; arg= els}
diff --git a/sledge/src/symbheap/term.ml b/sledge/src/symbheap/term.ml
index e8970b9da..633a46174 100644
--- a/sledge/src/symbheap/term.ml
+++ b/sledge/src/symbheap/term.ml
@@ -990,8 +990,6 @@ let rec simp_not (typ : Typ.t) term =
       simp_cond cnd (simp_not typ thn) (simp_not typ els)
   (* ¬false ==> true ¬true ==> false *)
   | Integer {data}, Integer {bits= 1} -> bool (Z.is_false data)
-  (* ¬b ==> false = b *)
-  | b, Integer {bits= 1} -> App {op= App {op= Eq; arg= bool false}; arg= b}
   (* ¬e ==> true xor e *)
   | e, _ ->
       App {op= App {op= Xor; arg= integer (Z.of_bool true) typ}; arg= e}