diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index a452d1046..6623875fb 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -96,6 +96,8 @@ module Formula = struct
 
   let inject b = b
   let project e = Some e
+  let tt = true_
+  let ff = false_
 
   let of_exp e =
     let b = Term.of_exp e in
diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
index 7717acbdc..85c409343 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol.mli
@@ -131,8 +131,8 @@ and Formula : sig
   (** Construct *)
 
   (* constants *)
-  val true_ : t
-  val false_ : t
+  val tt : t
+  val ff : t
 
   (* comparisons *)
   val eq : Term.t -> Term.t -> t
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 2afc46f4e..9af5becc2 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -33,7 +33,7 @@ let emp =
   { us= Var.Set.empty
   ; xs= Var.Set.empty
   ; ctx= Context.true_
-  ; pure= Formula.true_
+  ; pure= Formula.tt
   ; heap= []
   ; djns= [] }
 
@@ -508,7 +508,7 @@ let or_ q1 q2 =
       { us= Var.Set.union q1.us q2.us
       ; xs= Var.Set.empty
       ; ctx= Context.true_
-      ; pure= Formula.true_
+      ; pure= Formula.tt
       ; heap= []
       ; djns= [[q1; q2]] } )
   |>
@@ -553,7 +553,7 @@ let subst sub q =
   [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Var.Subst.pp sub pp q]
   ;
   let dom, eqs =
-    Var.Subst.fold sub ~init:(Var.Set.empty, Formula.true_)
+    Var.Subst.fold sub ~init:(Var.Set.empty, Formula.tt)
       ~f:(fun var trm (dom, eqs) ->
         ( Var.Set.add dom var
         , Formula.and_ (Formula.eq (Term.var var) (Term.var trm)) eqs ) )
diff --git a/sledge/src/solver.ml b/sledge/src/solver.ml
index 6d38ea570..26d26a90c 100644
--- a/sledge/src/solver.ml
+++ b/sledge/src/solver.ml
@@ -154,7 +154,7 @@ let excise_exists goal =
     let solutions_for_xs =
       let xs =
         Var.Set.diff goal.xs
-          (Sh.fv ~ignore_ctx:() (Sh.with_pure Formula.true_ goal.sub))
+          (Sh.fv ~ignore_ctx:() (Sh.with_pure Formula.tt goal.sub))
       in
       Context.solve_for_vars [Var.Set.empty; goal.us; xs] goal.sub.ctx
     in