diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml
index e6d32a52a..951f78b24 100644
--- a/sledge/src/exec.ml
+++ b/sledge/src/exec.ml
@@ -412,9 +412,9 @@ let realloc_spec reg ptr siz =
     Sh.or_
       (Sh.and_ (Formula.eq loc Term.zero) (Sh.rename sub foot))
       (Sh.and_
-         (Formula.conditional ~cnd:(Formula.le len siz)
-            ~thn:(eq_concat (siz, a1) [|(len, a0); (Term.sub siz len, a2)|])
-            ~els:(eq_concat (len, a0) [|(siz, a1); (Term.sub len siz, a2)|]))
+         (Formula.cond ~cnd:(Formula.le len siz)
+            ~pos:(eq_concat (siz, a1) [|(len, a0); (Term.sub siz len, a2)|])
+            ~neg:(eq_concat (len, a0) [|(siz, a1); (Term.sub len siz, a2)|]))
          (Sh.seg rseg))
   in
   {foot; sub; ms; post}
@@ -441,9 +441,9 @@ let rallocx_spec reg ptr siz =
     Sh.or_
       (Sh.and_ (Formula.eq loc Term.zero) (Sh.rename sub pheap))
       (Sh.and_
-         (Formula.conditional ~cnd:(Formula.le len siz)
-            ~thn:(eq_concat (siz, a1) [|(len, a0); (Term.sub siz len, a2)|])
-            ~els:(eq_concat (len, a0) [|(siz, a1); (Term.sub len siz, a2)|]))
+         (Formula.cond ~cnd:(Formula.le len siz)
+            ~pos:(eq_concat (siz, a1) [|(len, a0); (Term.sub siz len, a2)|])
+            ~neg:(eq_concat (len, a0) [|(siz, a1); (Term.sub len siz, a2)|]))
          (Sh.seg rseg))
   in
   {foot; sub; ms; post}
@@ -472,9 +472,9 @@ let xallocx_spec reg ptr siz ext =
   let post =
     Sh.and_
       (Formula.and_
-         (Formula.conditional ~cnd:(Formula.le len siz)
-            ~thn:(eq_concat (siz, a1) [|(len, a0); (Term.sub siz len, a2)|])
-            ~els:(eq_concat (len, a0) [|(siz, a1); (Term.sub len siz, a2)|]))
+         (Formula.cond ~cnd:(Formula.le len siz)
+            ~pos:(eq_concat (siz, a1) [|(len, a0); (Term.sub siz len, a2)|])
+            ~neg:(eq_concat (len, a0) [|(siz, a1); (Term.sub len siz, a2)|]))
          (Formula.and_ (Formula.le siz reg)
             (Formula.le reg (Term.add siz ext))))
       (Sh.seg seg')
diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 6623875fb..bde40a89b 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -98,6 +98,7 @@ module Formula = struct
   let project e = Some e
   let tt = true_
   let ff = false_
+  let cond ~cnd ~pos ~neg = conditional ~cnd ~thn:pos ~els:neg
 
   let of_exp e =
     let b = Term.of_exp e in
diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
index 85c409343..051d23ef9 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol.mli
@@ -144,7 +144,7 @@ and Formula : sig
   val not_ : t -> t
   val and_ : t -> t -> t
   val or_ : t -> t -> t
-  val conditional : cnd:t -> thn:t -> els:t -> t
+  val cond : cnd:t -> pos:t -> neg:t -> t
 
   (** Convert *)