diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml
index b9e99fbd6..e667f949a 100644
--- a/sledge/src/exec.ml
+++ b/sledge/src/exec.ml
@@ -87,7 +87,7 @@ let gen_spec us specm =
  * Instruction small axioms
  *)
 
-let null_eq ptr = Sh.pure (Formula.eq Term.zero ptr)
+let null_eq ptr = Sh.pure (Formula.eq0 ptr)
 
 let eq_concat (siz, seq) ms =
   Formula.eq (Term.sized ~siz ~seq)
@@ -156,8 +156,7 @@ let memcpy_eq_spec dst src len =
   let+ seg = Fresh.seg dst ~len in
   let dst_heap = Sh.seg seg in
   let foot =
-    Sh.and_ (Formula.eq dst src)
-      (Sh.and_ (Formula.eq len Term.zero) dst_heap)
+    Sh.and_ (Formula.eq dst src) (Sh.and_ (Formula.eq0 len) dst_heap)
   in
   let post = dst_heap in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
@@ -336,7 +335,7 @@ let malloc_spec reg siz =
  * { r=0 ∨ ∃α'. r-[r;sΘ)->⟨sΘ,α'⟩ }
  *)
 let mallocx_spec reg siz =
-  let foot = Sh.pure (Formula.dq siz Term.zero) in
+  let foot = Sh.pure (Formula.dq0 siz) in
   let* sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:(Term.fv siz) in
   let loc = Term.var reg in
   let siz = Term.rename sub siz in
@@ -410,7 +409,7 @@ let realloc_spec reg ptr siz =
   let+ a2 = Fresh.var "a" in
   let post =
     Sh.or_
-      (Sh.and_ (Formula.eq loc Term.zero) (Sh.rename sub foot))
+      (Sh.and_ (Formula.eq0 loc) (Sh.rename sub foot))
       (Sh.and_
          (Formula.cond ~cnd:(Formula.le len siz)
             ~pos:(eq_concat (siz, a1) [|(len, a0); (Term.sub siz len, a2)|])
@@ -429,7 +428,7 @@ let rallocx_spec reg ptr siz =
   let* len = Fresh.var "m" in
   let* pseg = Fresh.seg ptr ~bas:ptr ~len ~siz:len in
   let pheap = Sh.seg pseg in
-  let foot = Sh.and_ (Formula.dq siz Term.zero) pheap in
+  let foot = Sh.and_ (Formula.dq0 siz) pheap in
   let* sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:foot.us in
   let loc = Term.var reg in
   let siz = Term.rename sub siz in
@@ -439,7 +438,7 @@ let rallocx_spec reg ptr siz =
   let+ a2 = Fresh.var "a" in
   let post =
     Sh.or_
-      (Sh.and_ (Formula.eq loc Term.zero) (Sh.rename sub pheap))
+      (Sh.and_ (Formula.eq0 loc) (Sh.rename sub pheap))
       (Sh.and_
          (Formula.cond ~cnd:(Formula.le len siz)
             ~pos:(eq_concat (siz, a1) [|(len, a0); (Term.sub siz len, a2)|])
@@ -456,7 +455,7 @@ let rallocx_spec reg ptr siz =
 let xallocx_spec reg ptr siz ext =
   let* len = Fresh.var "m" in
   let* seg = Fresh.seg ptr ~bas:ptr ~len ~siz:len in
-  let foot = Sh.and_ (Formula.dq siz Term.zero) (Sh.seg seg) in
+  let foot = Sh.and_ (Formula.dq0 siz) (Sh.seg seg) in
   let* sub, ms =
     Fresh.assign ~ws:(Var.Set.of_ reg)
       ~rs:Var.Set.(union foot.us (union (Term.fv siz) (Term.fv ext)))
@@ -510,7 +509,7 @@ let malloc_usable_size_spec reg ptr =
  * { r=0 ∨ r=sΘ }
  *)
 let nallocx_spec reg siz =
-  let foot = Sh.pure (Formula.dq siz Term.zero) in
+  let foot = Sh.pure (Formula.dq0 siz) in
   let+ sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:foot.us in
   let loc = Term.var reg in
   let siz = Term.rename sub siz in
@@ -528,9 +527,8 @@ let mallctl_read_spec r i w n =
   let* rseg = Fresh.seg r ~siz:iseg.seq in
   let+ a = Fresh.var "a" in
   let foot =
-    Sh.and_ (Formula.eq w Term.zero)
-      (Sh.and_ (Formula.eq n Term.zero)
-         (Sh.star (Sh.seg iseg) (Sh.seg rseg)))
+    Sh.and_ (Formula.eq0 w)
+      (Sh.and_ (Formula.eq0 n) (Sh.star (Sh.seg iseg) (Sh.seg rseg)))
   in
   let rseg' = {rseg with seq= a} in
   let post = Sh.star (Sh.seg rseg') (Sh.seg iseg) in
@@ -550,8 +548,8 @@ let mallctlbymib_read_spec p l r i w n =
   let const = Sh.star (Sh.seg pseg) (Sh.seg iseg) in
   let+ a = Fresh.var "a" in
   let foot =
-    Sh.and_ (Formula.eq w Term.zero)
-      (Sh.and_ (Formula.eq n Term.zero) (Sh.star const (Sh.seg rseg)))
+    Sh.and_ (Formula.eq0 w)
+      (Sh.and_ (Formula.eq0 n) (Sh.star const (Sh.seg rseg)))
   in
   let rseg' = {rseg with seq= a} in
   let post = Sh.star (Sh.seg rseg') const in
@@ -564,9 +562,7 @@ let mallctlbymib_read_spec p l r i w n =
 let mallctl_write_spec r i w n =
   let+ seg = Fresh.seg w ~siz:n in
   let post = Sh.seg seg in
-  let foot =
-    Sh.and_ (Formula.eq r Term.zero) (Sh.and_ (Formula.eq i Term.zero) post)
-  in
+  let foot = Sh.and_ (Formula.eq0 r) (Sh.and_ (Formula.eq0 i) post) in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
 (* { p-[_;_)->⟨W×l,_⟩ * r=0 * i=0 * w-[_;_)->⟨n,_⟩ }
@@ -579,9 +575,7 @@ let mallctlbymib_write_spec p l r i w n =
   let* pseg = Fresh.seg p ~siz:wl in
   let+ wseg = Fresh.seg w ~siz:n in
   let post = Sh.star (Sh.seg pseg) (Sh.seg wseg) in
-  let foot =
-    Sh.and_ (Formula.eq r Term.zero) (Sh.and_ (Formula.eq i Term.zero) post)
-  in
+  let foot = Sh.and_ (Formula.eq0 r) (Sh.and_ (Formula.eq0 i) post) in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
 let mallctl_specs r i w n =
diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 3087de7cb..cd921d26d 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -133,8 +133,12 @@ type fml =
   | Ff
   | Eq of trm * trm
   | Dq of trm * trm
-  | Lt of trm * trm
-  | Le of trm * trm
+  | Eq0 of trm  (** [Eq0(x)] iff x = 0 *)
+  | Dq0 of trm  (** [Dq0(x)] iff x ≠ 0 *)
+  | Gt0 of trm  (** [Gt0(x)] iff x > 0 *)
+  | Ge0 of trm  (** [Ge0(x)] iff x ≥ 0 *)
+  | Lt0 of trm  (** [Lt0(x)] iff x < 0 *)
+  | Le0 of trm  (** [Le0(x)] iff x ≤ 0 *)
   | And of fml * fml
   | Or of fml * fml
   | Iff of fml * fml
@@ -146,8 +150,12 @@ type fml =
 
 let _Eq x y = Eq (x, y)
 let _Dq x y = Dq (x, y)
-let _Lt x y = Lt (x, y)
-let _Le x y = Le (x, y)
+let _Eq0 x = Eq0 x
+let _Dq0 x = Dq0 x
+let _Gt0 x = Gt0 x
+let _Ge0 x = Ge0 x
+let _Lt0 x = Lt0 x
+let _Le0 x = Le0 x
 let _And p q = And (p, q)
 let _Or p q = Or (p, q)
 let _Iff p q = Iff (p, q)
@@ -461,8 +469,12 @@ let ppx_f strength fs fml =
     | Ff -> pf "ff"
     | Eq (x, y) -> pf "(%a@ = %a)" pp_t x pp_t y
     | Dq (x, y) -> pf "(%a@ @<2>≠ %a)" pp_t x pp_t y
-    | Lt (x, y) -> pf "(%a@ < %a)" pp_t x pp_t y
-    | Le (x, y) -> pf "(%a@ @<2>≤ %a)" pp_t x pp_t y
+    | Eq0 x -> pf "(0 = %a)" pp_t x
+    | Dq0 x -> pf "(0 @<2>≠ %a)" pp_t x
+    | Gt0 x -> pf "(0 < %a)" pp_t x
+    | Ge0 x -> pf "(0 @<2>≤ %a)" pp_t x
+    | Lt0 x -> pf "(0 > %a)" pp_t x
+    | Le0 x -> pf "(0 @<2>≥ %a)" pp_t x
     | And (x, y) -> pf "(%a@ @<2>∧ %a)" pp x pp y
     | Or (x, y) -> pf "(%a@ @<2>∨ %a)" pp x pp y
     | Iff (x, y) -> pf "(%a@ <=> %a)" pp x pp y
@@ -518,8 +530,8 @@ let rec fold_vars_t e ~init ~f =
 let rec fold_vars_f ~init p ~f =
   match (p : fml) with
   | Tt | Ff -> init
-  | Eq (x, y) | Dq (x, y) | Lt (x, y) | Le (x, y) ->
-      fold_vars_t ~f x ~init:(fold_vars_t ~f y ~init)
+  | Eq (x, y) | Dq (x, y) -> fold_vars_t ~f x ~init:(fold_vars_t ~f y ~init)
+  | Eq0 x | Dq0 x | Gt0 x | Ge0 x | Lt0 x | Le0 x -> fold_vars_t ~f x ~init
   | And (x, y) | Or (x, y) | Iff (x, y) | Xor (x, y) ->
       fold_vars_f ~f x ~init:(fold_vars_f ~f y ~init)
   | Cond {cnd; pos; neg} ->
@@ -582,8 +594,12 @@ let rec map_vars_f ~f e =
   | Tt | Ff -> e
   | Eq (x, y) -> map2 (map_vars_t ~f) e _Eq x y
   | Dq (x, y) -> map2 (map_vars_t ~f) e _Dq x y
-  | Lt (x, y) -> map2 (map_vars_t ~f) e _Lt x y
-  | Le (x, y) -> map2 (map_vars_t ~f) e _Le x y
+  | Eq0 x -> map1 (map_vars_t ~f) e _Eq0 x
+  | Dq0 x -> map1 (map_vars_t ~f) e _Dq0 x
+  | Gt0 x -> map1 (map_vars_t ~f) e _Gt0 x
+  | Ge0 x -> map1 (map_vars_t ~f) e _Ge0 x
+  | Lt0 x -> map1 (map_vars_t ~f) e _Lt0 x
+  | Le0 x -> map1 (map_vars_t ~f) e _Le0 x
   | And (x, y) -> map2 (map_vars_f ~f) e _And x y
   | Or (x, y) -> map2 (map_vars_f ~f) e _Or x y
   | Iff (x, y) -> map2 (map_vars_f ~f) e _Iff x y
@@ -699,6 +715,9 @@ let ap1 : (trm -> exp) -> exp -> exp =
 
 let ap1t : (trm -> trm) -> exp -> exp = fun f -> ap1 (fun x -> `Trm (f x))
 
+let ap1f : (trm -> fml) -> exp -> fml =
+ fun f x -> map_cnd _Cond f (embed_into_cnd x)
+
 (** Map a binary function on terms over conditional terms. This yields a
     conditional tree with the structure from the first argument where each
     leaf has been replaced by a conditional tree with the structure from the
@@ -908,8 +927,25 @@ module Formula = struct
 
   let eq = ap2f _Eq
   let dq = ap2f _Dq
-  let lt = ap2f _Lt
-  let le = ap2f _Le
+  let eq0 = ap1f _Eq0
+  let dq0 = ap1f _Dq0
+  let gt0 = ap1f _Gt0
+  let ge0 = ap1f _Ge0
+  let lt0 = ap1f _Lt0
+  let le0 = ap1f _Le0
+
+  let gt a b =
+    if a == Term.zero then lt0 b
+    else if b == Term.zero then gt0 a
+    else gt0 (Term.sub a b)
+
+  let ge a b =
+    if a == Term.zero then le0 b
+    else if b == Term.zero then ge0 a
+    else ge0 (Term.sub a b)
+
+  let lt a b = gt b a
+  let le a b = ge b a
 
   (* connectives *)
 
@@ -926,8 +962,12 @@ module Formula = struct
     | Ff -> Tt
     | Eq (x, y) -> Dq (x, y)
     | Dq (x, y) -> Eq (x, y)
-    | Lt (x, y) -> Le (y, x)
-    | Le (x, y) -> Lt (y, x)
+    | Eq0 x -> Dq0 x
+    | Dq0 x -> Eq0 x
+    | Gt0 x -> Le0 x
+    | Ge0 x -> Lt0 x
+    | Lt0 x -> Ge0 x
+    | Le0 x -> Gt0 x
     | And (x, y) -> Or (not_ x, not_ y)
     | Or (x, y) -> And (not_ x, not_ y)
     | Iff (x, y) -> Xor (x, y)
@@ -1043,8 +1083,12 @@ let rec f_to_ses : fml -> Ses.Term.t = function
   | Ff -> Ses.Term.false_
   | Eq (x, y) -> Ses.Term.eq (t_to_ses x) (t_to_ses y)
   | Dq (x, y) -> Ses.Term.dq (t_to_ses x) (t_to_ses y)
-  | Lt (x, y) -> Ses.Term.lt (t_to_ses x) (t_to_ses y)
-  | Le (x, y) -> Ses.Term.le (t_to_ses x) (t_to_ses y)
+  | Eq0 x -> Ses.Term.eq Ses.Term.zero (t_to_ses x)
+  | Dq0 x -> Ses.Term.dq Ses.Term.zero (t_to_ses x)
+  | Gt0 x -> Ses.Term.lt Ses.Term.zero (t_to_ses x)
+  | Ge0 x -> Ses.Term.le Ses.Term.zero (t_to_ses x)
+  | Lt0 x -> Ses.Term.lt (t_to_ses x) Ses.Term.zero
+  | Le0 x -> Ses.Term.le (t_to_ses x) Ses.Term.zero
   | And (p, q) -> Ses.Term.and_ (f_to_ses p) (f_to_ses q)
   | Or (p, q) -> Ses.Term.or_ (f_to_ses p) (f_to_ses q)
   | Iff (p, q) -> Ses.Term.eq (f_to_ses p) (f_to_ses q)
@@ -1467,13 +1511,13 @@ module Term_of_Llair = struct
         ap_fff (fun p q -> or_ p (not_ q)) p q
     | Ap2 (Eq, _, d, e) -> ap_ttf eq d e
     | Ap2 (Dq, _, d, e) -> ap_ttf dq d e
-    | Ap2 (Gt, _, d, e) -> ap_ttf lt e d
+    | Ap2 (Gt, _, d, e) -> ap_ttf gt d e
     | Ap2 (Lt, _, d, e) -> ap_ttf lt d e
-    | Ap2 (Ge, _, d, e) -> ap_ttf le e d
+    | Ap2 (Ge, _, d, e) -> ap_ttf ge d e
     | Ap2 (Le, _, d, e) -> ap_ttf le d e
-    | Ap2 (Ugt, typ, d, e) -> usap_ttf lt typ e d
+    | Ap2 (Ugt, typ, d, e) -> usap_ttf gt typ d e
     | Ap2 (Ult, typ, d, e) -> usap_ttf lt typ d e
-    | Ap2 (Uge, typ, d, e) -> usap_ttf le typ e d
+    | Ap2 (Uge, typ, d, e) -> usap_ttf ge typ d e
     | Ap2 (Ule, typ, d, e) -> usap_ttf le typ d e
     | Ap2 (Ord, _, d, e) -> ap_ttf (upos2 Ordered) d e
     | Ap2 (Uno, _, d, e) -> ap_ttf (uneg2 Ordered) d e
diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
index 74b17f80b..b74838754 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol.mli
@@ -145,6 +145,14 @@ and Formula : sig
   (* comparisons *)
   val eq : Term.t -> Term.t -> t
   val dq : Term.t -> Term.t -> t
+  val eq0 : Term.t -> t
+  val dq0 : Term.t -> t
+  val gt0 : Term.t -> t
+  val ge0 : Term.t -> t
+  val lt0 : Term.t -> t
+  val le0 : Term.t -> t
+  val gt : Term.t -> Term.t -> t
+  val ge : Term.t -> Term.t -> t
   val lt : Term.t -> Term.t -> t
   val le : Term.t -> Term.t -> t
 
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 6dfbbf924..fc2e78373 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -587,8 +587,7 @@ let rec pure_approx q =
   Formula.andN
     ( [q.pure]
     |> fun init ->
-    List.fold ~init q.heap ~f:(fun p seg ->
-        Formula.dq Term.zero seg.loc :: p )
+    List.fold ~init q.heap ~f:(fun p seg -> Formula.dq0 seg.loc :: p)
     |> fun init ->
     List.fold ~init q.djns ~f:(fun p djn ->
         Formula.orN (List.map djn ~f:pure_approx) :: p ) )
diff --git a/sledge/src/solver_test.ml b/sledge/src/solver_test.ml
index 7282cb815..a8dd4d0d9 100644
--- a/sledge/src/solver_test.ml
+++ b/sledge/src/solver_test.ml
@@ -270,7 +270,7 @@ let%test_module _ =
       [%expect
         {|
         ( infer_frame:
-            (%n_9 ≤ 2)
+            (0 ≤ (2 + (-1 × %n_9)))
           ∧ %l_6
               -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(16 + (-8 × %n_9)),%a_3⟩
           \- ∃ %a_1, %m_8 .