diff --git a/src/arith/sidekick_arith.ml b/src/arith/sidekick_arith.ml
index 86433456..a6c11621 100644
--- a/src/arith/sidekick_arith.ml
+++ b/src/arith/sidekick_arith.ml
@@ -45,6 +45,14 @@ module type RATIONAL = sig
   val num : t -> bigint
   val denum : t -> bigint
 
+  val infinity : t
+  (** +infinity *)
+
+  val minus_infinity : t
+
+  val is_real : t -> bool
+  (** A proper real, not nan/infinity *)
+
   val pp_approx : int -> Format.formatter -> t -> unit
   (** Pretty print rational with given amount of precision
       (for example as a floating point number) *)
diff --git a/src/lra/simplex2.ml b/src/lra/simplex2.ml
index 24aef8ed..d4c2b272 100644
--- a/src/lra/simplex2.ml
+++ b/src/lra/simplex2.ml
@@ -217,8 +217,8 @@ module Make(Q : RATIONAL)(Var: VAR)
     let[@inline] (>=) a b = compare a b >= 0
     let[@inline] (=) a b = compare a b = 0
 
-    let plus_inf = make Q.inf Q.zero
-    let minus_inf = make Q.minus_inf Q.zero
+    let plus_inf = make Q.infinity Q.zero
+    let minus_inf = make Q.minus_infinity Q.zero
     let[@inline] min x y = if x <= y then x else y
     let[@inline] max x y = if x >= y then x else y
 
diff --git a/src/zarith/sidekick_zarith.ml b/src/zarith/sidekick_zarith.ml
index 00601f4c..a3260b96 100644
--- a/src/zarith/sidekick_zarith.ml
+++ b/src/zarith/sidekick_zarith.ml
@@ -15,6 +15,10 @@ module Rational
   let pp = pp_print
   let hash a = Hashtbl.hash (Z.hash (num a), Z.hash (den a))
 
+  let infinity = Q.inf
+  let minus_infinity = Q.minus_inf
+  let is_real = Q.is_real
+
   let pp_approx n out q = Format.fprintf out "%*.1f" n (Q.to_float q)
 end