diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 66c583fa6..9c75c4cfe 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -1119,7 +1119,6 @@ let rec t_to_ses : trm -> Ses.Term.t = function
       Ses.Term.update ~rcd:(t_to_ses rcd)
         ~idx:(to_int (t_to_ses idx))
         ~elt:(t_to_ses elt)
-  | Apply (Float s, Tuple [||]) -> Ses.Term.float s
   | Apply (Label {parent; name}, Tuple [||]) -> Ses.Term.label ~parent ~name
   | Apply (Mul, Tuple [|x; y|]) -> Ses.Term.mul (t_to_ses x) (t_to_ses y)
   | Apply (Div, Tuple [|x; y|]) -> Ses.Term.div (t_to_ses x) (t_to_ses y)
@@ -1229,7 +1228,6 @@ and of_ses : Ses.Term.t -> exp =
   | Var {id; name} -> var (Var.identified ~id ~name)
   | Integer {data} -> integer data
   | Rational {data} -> rational data
-  | Float {data} -> uap0 (Float data)
   | Label {parent; name} -> uap0 (Label {parent; name})
   | Ap1 (Signed {bits}, e) -> uap_tt (Signed bits) e
   | Ap1 (Unsigned {bits}, e) -> uap_tt (Unsigned bits) e
@@ -1606,7 +1604,8 @@ module Term_of_Llair = struct
     | Float {data; typ= _} -> (
       match Q.of_float (Float.of_string data) with
       | q when Q.is_real q -> rational q
-      | _ | (exception Invalid_argument _) -> uap0 (Float data) )
+      | _ | (exception Invalid_argument _) ->
+          uap0 (Uninterp ("float_" ^ data)) )
     | Ap1 (Signed {bits}, _, e) ->
         let a = exp e in
         if bits = 1 then
diff --git a/sledge/src/ses/equality.ml b/sledge/src/ses/equality.ml
index e472507ad..68809da5d 100644
--- a/sledge/src/ses/equality.ml
+++ b/sledge/src/ses/equality.ml
@@ -19,8 +19,7 @@ let classify e =
   | Mul _ | Ap1 _ | Ap2 _ | Ap3 _ | ApN _ | Apply _ | PosLit _ | NegLit _
    |And _ | Or _ ->
       Uninterpreted
-  | Var _ | Integer _ | Rational _ | Float _ | Label _ | RecRecord _ ->
-      Atomic
+  | Var _ | Integer _ | Rational _ | Label _ | RecRecord _ -> Atomic
 
 let interpreted e = equal_kind (classify e) Interpreted
 let non_interpreted e = not (interpreted e)
@@ -102,7 +101,7 @@ end = struct
   (** compose a substitution with a mapping *)
   let compose1 ~key ~data s =
     match (key : Term.t) with
-    | Integer _ | Rational _ | Float _ | Label _ -> s
+    | Integer _ | Rational _ | Label _ -> s
     | _ ->
         if Term.equal key data then s
         else compose s (Term.Map.singleton key data)
@@ -135,7 +134,7 @@ end = struct
         else
           let s = Term.Map.remove s key in
           match (key : Term.t) with
-          | Integer _ | Rational _ | Float _ | Label _ -> s
+          | Integer _ | Rational _ | Label _ -> s
           | _ -> Term.Map.add_exn ~key:key' ~data:data' s )
 
   (** Holds only if [true ⊢ ∃xs. e=f]. Clients assume
@@ -478,7 +477,7 @@ let rec canon r a =
 
 let rec extend_ a r =
   match (a : Term.t) with
-  | Integer _ | Rational _ | Float _ | Label _ -> r
+  | Integer _ | Rational _ | Label _ -> r
   | _ -> (
       if interpreted a then Term.fold ~f:extend_ a ~init:r
       else
diff --git a/sledge/src/ses/funsym.ml b/sledge/src/ses/funsym.ml
index c46f25c5d..4e2d10637 100644
--- a/sledge/src/ses/funsym.ml
+++ b/sledge/src/ses/funsym.ml
@@ -8,7 +8,6 @@
 (** Function Symbols *)
 
 type t =
-  | Float of string
   | Label of {parent: string; name: string}
   | Mul
   | Div
@@ -30,7 +29,6 @@ type t =
 let pp ppf f =
   let pf fmt = Format.fprintf ppf fmt in
   match f with
-  | Float s -> pf "%s" s
   | Label {name} -> pf "%s" name
   | Mul -> pf "@<1>×"
   | Div -> pf "/"
diff --git a/sledge/src/ses/funsym.mli b/sledge/src/ses/funsym.mli
index c8cc681fb..cbc62a77b 100644
--- a/sledge/src/ses/funsym.mli
+++ b/sledge/src/ses/funsym.mli
@@ -12,7 +12,6 @@
     applied to literal values of the expected sorts are reduced to literal
     values. *)
 type t =
-  | Float of string
   | Label of {parent: string; name: string}
   | Mul  (** Multiplication *)
   | Div  (** Division, for integers result is truncated toward zero *)
diff --git a/sledge/src/ses/term.ml b/sledge/src/ses/term.ml
index aa9fdbc42..4905e6513 100644
--- a/sledge/src/ses/term.ml
+++ b/sledge/src/ses/term.ml
@@ -69,7 +69,6 @@ and T : sig
     | Add of qset
     | Mul of qset
     | Label of {parent: string; name: string}
-    | Float of {data: string}
     | Integer of {data: Z.t}
     | Rational of {data: Q.t}
     | RecRecord of int
@@ -92,7 +91,6 @@ end = struct
     | Add of qset
     | Mul of qset
     | Label of {parent: string; name: string}
-    | Float of {data: string}
     | Integer of {data: Z.t}
     | Rational of {data: Q.t}
     | RecRecord of int
@@ -260,7 +258,6 @@ let rec ppx strength fs term =
     | Var _ as v -> Var.ppx strength fs (Var.of_ v)
     | Integer {data} -> Trace.pp_styled `Magenta "%a" fs Z.pp data
     | Rational {data} -> Trace.pp_styled `Magenta "%a" fs Q.pp data
-    | Float {data} -> pf "%s" data
     | Label {name} -> pf "%s" name
     | Ap1 (Signed {bits}, arg) -> pf "((s%i)@ %a)" bits pp arg
     | Ap1 (Unsigned {bits}, arg) -> pf "((u%i)@ %a)" bits pp arg
@@ -358,7 +355,6 @@ let minus_one = integer Z.minus_one
 let bool b = integer (Z.of_bool b)
 let true_ = bool true
 let false_ = bool false
-let float data = Float {data} |> check invariant
 let label ~parent ~name = Label {parent; name} |> check invariant
 
 (* type conversions *)
@@ -1044,7 +1040,7 @@ let map e ~f =
   | Apply (sym, xs) -> mapN (simp_apply sym) ~f xs
   | PosLit (sym, xs) -> mapN (simp_poslit sym) ~f xs
   | NegLit (sym, xs) -> mapN (simp_neglit sym) ~f xs
-  | Var _ | Label _ | Float _ | Integer _ | Rational _ | RecRecord _ -> e
+  | Var _ | Label _ | Integer _ | Rational _ | RecRecord _ -> e
 
 let fold_map e ~init ~f =
   let s = ref init in
@@ -1099,7 +1095,7 @@ let iter e ~f =
       IArray.iter ~f xs
   | And args | Or args -> Set.iter ~f args
   | Add args | Mul args -> Qset.iter ~f:(fun arg _ -> f arg) args
-  | Var _ | Label _ | Float _ | Integer _ | Rational _ | RecRecord _ -> ()
+  | Var _ | Label _ | Integer _ | Rational _ | RecRecord _ -> ()
 
 let exists e ~f =
   match e with
@@ -1110,8 +1106,7 @@ let exists e ~f =
       IArray.exists ~f xs
   | And args | Or args -> Set.exists ~f args
   | Add args | Mul args -> Qset.exists ~f:(fun arg _ -> f arg) args
-  | Var _ | Label _ | Float _ | Integer _ | Rational _ | RecRecord _ ->
-      false
+  | Var _ | Label _ | Integer _ | Rational _ | RecRecord _ -> false
 
 let for_all e ~f =
   match e with
@@ -1122,7 +1117,7 @@ let for_all e ~f =
       IArray.for_all ~f xs
   | And args | Or args -> Set.for_all ~f args
   | Add args | Mul args -> Qset.for_all ~f:(fun arg _ -> f arg) args
-  | Var _ | Label _ | Float _ | Integer _ | Rational _ | RecRecord _ -> true
+  | Var _ | Label _ | Integer _ | Rational _ | RecRecord _ -> true
 
 let fold e ~init:s ~f =
   match e with
@@ -1133,7 +1128,7 @@ let fold e ~init:s ~f =
       IArray.fold ~f:(fun s x -> f x s) xs ~init:s
   | And args | Or args -> Set.fold ~f:(fun s e -> f e s) args ~init:s
   | Add args | Mul args -> Qset.fold ~f:(fun e _ s -> f e s) args ~init:s
-  | Var _ | Label _ | Float _ | Integer _ | Rational _ | RecRecord _ -> s
+  | Var _ | Label _ | Integer _ | Rational _ | RecRecord _ -> s
 
 let rec iter_terms e ~f =
   ( match e with
@@ -1150,8 +1145,7 @@ let rec iter_terms e ~f =
   | And args | Or args -> Set.iter args ~f:(iter_terms ~f)
   | Add args | Mul args ->
       Qset.iter args ~f:(fun arg _ -> iter_terms ~f arg)
-  | Var _ | Label _ | Float _ | Integer _ | Rational _ | RecRecord _ -> ()
-  ) ;
+  | Var _ | Label _ | Integer _ | Rational _ | RecRecord _ -> () ) ;
   f e
 
 let rec fold_terms e ~init:s ~f =
@@ -1167,7 +1161,7 @@ let rec fold_terms e ~init:s ~f =
         Set.fold args ~init:s ~f:(fun s x -> fold_terms f x s)
     | Add args | Mul args ->
         Qset.fold args ~init:s ~f:(fun arg _ s -> fold_terms f arg s)
-    | Var _ | Label _ | Float _ | Integer _ | Rational _ | RecRecord _ -> s
+    | Var _ | Label _ | Integer _ | Rational _ | RecRecord _ -> s
   in
   f s e
 
@@ -1190,7 +1184,7 @@ let is_false = function Integer {data} -> Z.is_false data | _ -> false
 
 let rec is_constant = function
   | Var _ -> false
-  | Label _ | Float _ | Integer _ | Rational _ -> true
+  | Label _ | Integer _ | Rational _ -> true
   | a -> for_all ~f:is_constant a
 
 let rec height = function
@@ -1204,7 +1198,7 @@ let rec height = function
       1 + Set.fold bs ~init:0 ~f:(fun m a -> max m (height a))
   | Add qs | Mul qs ->
       1 + Qset.fold qs ~init:0 ~f:(fun a _ m -> max m (height a))
-  | Label _ | Float _ | Integer _ | Rational _ | RecRecord _ -> 0
+  | Label _ | Integer _ | Rational _ | RecRecord _ -> 0
 
 (** Solve *)
 
diff --git a/sledge/src/ses/term.mli b/sledge/src/ses/term.mli
index 6a778efa7..05ee94359 100644
--- a/sledge/src/ses/term.mli
+++ b/sledge/src/ses/term.mli
@@ -85,7 +85,6 @@ and T : sig
     | Mul of qset  (** Product of terms with rational exponents *)
     | Label of {parent: string; name: string}
         (** Address of named code block within parent function *)
-    | Float of {data: string}  (** Floating-point constant *)
     | Integer of {data: Z.t}  (** Integer constant *)
     | Rational of {data: Q.t}  (** Rational constant *)
     | RecRecord of int  (** Reference to ancestor recursive record *)
@@ -134,7 +133,6 @@ val zero : t
 val one : t
 val minus_one : t
 val rational : Q.t -> t
-val float : string -> t
 
 (* type conversions *)
 val signed : int -> t -> t