From 425711459d5ca007581fc299d90f752abf6baef7 Mon Sep 17 00:00:00 2001
From: Tiago Ferreira <me@tiferrei.com>
Date: Tue, 9 Dec 2025 17:04:48 +0000
Subject: [PATCH 1/5] checkin

---
 src/smtml/eval.ml                | 161 ++++++++++++++++++++++++-------
 src/smtml/eval.mli               |   1 +
 src/smtml/expr.ml                |  12 ++-
 src/smtml/mappings.ml            |   4 +-
 src/smtml/mappings_intf.ml       |   4 +-
 src/smtml/parser.mly             |   2 +-
 src/smtml/smtlib.ml              |   5 +-
 src/smtml/value.ml               |  30 ++++--
 src/smtml/value.mli              |   5 +-
 src/smtml/z3_mappings.default.ml |   8 +-
 test/cli/smtml/test_smtml.t      |   4 +-
 test/unit/test_eval.ml           |  73 +++++++++-----
 test/unit/test_expr.ml           |  78 ++++++++++++---
 test/unit/test_model.ml          |   2 +-
 14 files changed, 291 insertions(+), 98 deletions(-)

diff --git a/src/smtml/eval.ml b/src/smtml/eval.ml
index f59dc813..b668f05c 100644
--- a/src/smtml/eval.ml
+++ b/src/smtml/eval.ml
@@ -38,6 +38,7 @@ type error_kind =
   | `Integer_overflow
   | `Index_out_of_bounds
   | `Invalid_format_conversion
+  | `Negative_sqrt
   | `Unsupported_operator of op_type * Ty.t
   | `Unsupported_theory of Ty.t
   | `Type_error of type_error_info
@@ -194,63 +195,151 @@ module Int = struct
   let cvtop (op : Ty.Cvtop.t) (v : Value.t) : Value.t =
     match op with
     | OfBool -> to_int (of_bool v)
-    | Reinterpret_float -> Int (Int.of_float (of_real 1 (`Cvtop op) v))
+    | Reinterpret_float -> Int begin
+      match (of_real 1 (`Cvtop op) v) with
+        | Exact v -> Q.to_int v
+        | Approx v -> Int.of_float v
+    end
     | _ -> eval_error (`Unsupported_operator (`Cvtop op, Ty_int))
 end
 
 module Real = struct
   let unop (op : Ty.Unop.t) (v : Value.t) : Value.t =
     let v = of_real 1 (`Unop op) v in
-    match op with
-    | Neg -> to_real @@ Float.neg v
-    | Abs -> to_real @@ Float.abs v
-    | Sqrt -> to_real @@ Float.sqrt v
-    | Nearest -> to_real @@ Float.round v
-    | Ceil -> to_real @@ Float.ceil v
-    | Floor -> to_real @@ Float.floor v
-    | Trunc -> to_real @@ Float.trunc v
-    | Is_nan -> if Float.is_nan v then Value.True else Value.False
-    | _ -> eval_error (`Unsupported_operator (`Unop op, Ty_real))
+    let sqrt_q (q : Q.t) =
+      let n = Q.num q in
+      let d = Q.den q in
+      if Z.sign n < 0
+        then eval_error (`Negative_sqrt)
+      else
+        let (n_root, n_rem) = Z.sqrt_rem n in
+        let (d_root, d_rem) = Z.sqrt_rem d in
+        if Z.equal n_rem Z.zero && Z.equal d_rem Z.zero then
+          to_real (Exact (Q.make n_root d_root))
+        else
+          to_real (Approx (Q.to_float q |> sqrt)) in
+    let nearest_q (q : Q.t) =
+      let n = Q.num q in
+      let d = Q.den q in
+      let near = if Z.geq n Z.zero
+        then Z.div (Z.add n (Z.div d (Z.of_int 2))) d
+        else Z.div (Z.sub n (Z.div d (Z.of_int 2))) d in
+      to_real (Exact (Q.of_bigint near)) in
+    let approx_ops = fun v ->
+      let to_real v = to_real (Approx v) in
+      match op with
+      | Neg -> to_real @@ Float.neg v
+      | Abs -> to_real @@ Float.abs v
+      | Sqrt -> to_real @@ Float.sqrt v
+      | Nearest -> to_real @@ Float.round v
+      | Ceil -> to_real @@ Float.ceil v
+      | Floor -> to_real @@ Float.floor v
+      | Trunc -> to_real @@ Float.trunc v
+      | Is_nan -> if Float.is_nan v then Value.True else Value.False
+      | _ -> eval_error (`Unsupported_operator (`Unop op, Ty_real)) in
+    let exact_ops = fun v ->
+      let to_real v = to_real (Exact v) in
+      match op with
+      | Neg -> to_real @@ Q.neg v
+      | Abs -> to_real @@ Q.abs v
+      | Sqrt -> sqrt_q v
+      | Nearest -> nearest_q v
+      | Ceil -> to_real @@ Q.of_bigint @@ Z.cdiv (Q.num v) (Q.den v)
+      | Floor -> to_real @@ Q.of_bigint @@ Z.fdiv (Q.num v) (Q.den v)
+      | Trunc -> to_real @@ Q.of_bigint @@ Z.div (Q.num v) (Q.den v)
+      | Is_nan -> (match Q.classify v with
+        | Q.UNDEF -> Value.True
+        | _ -> Value.False)
+      | _ -> eval_error (`Unsupported_operator (`Unop op, Ty_real)) in
+    match v with
+      | Exact v -> exact_ops v
+      | Approx v -> approx_ops v
 
   let binop (op : Ty.Binop.t) (v1 : Value.t) (v2 : Value.t) : Value.t =
-    let f =
-      match op with
-      | Add -> Float.add
-      | Sub -> Float.sub
-      | Mul -> Float.mul
-      | Div -> Float.div
-      | Rem -> Float.rem
-      | Min -> Float.min
-      | Max -> Float.max
-      | Pow -> Float.pow
-      | _ -> eval_error (`Unsupported_operator (`Binop op, Ty_real))
-    in
-    to_real (f (of_real 1 (`Binop op) v1) (of_real 2 (`Binop op) v2))
+    let rem_q (a : Q.t) (b : Q.t) : Q.t =
+      if Q.equal b Q.zero then eval_error (`Divide_by_zero);
+      let div = Q.div a b in
+      let k = Q.of_bigint (Z.div (Q.num div) (Q.den div)) in
+      Q.sub a (Q.mul b k) in
+    let approx_op v1 v2 : Value.real = match op with
+      | Add -> Approx (Float.add v1 v2)
+      | Sub -> Approx (Float.sub v1 v2)
+      | Mul -> Approx (Float.mul v1 v2)
+      | Div -> Approx (Float.div v1 v2)
+      | Rem -> Approx (Float.rem v1 v2)
+      | Min -> Approx (Float.min v1 v2)
+      | Max -> Approx (Float.max v1 v2)
+      | Pow -> Approx (Float.pow v1 v2)
+      | _ -> eval_error (`Unsupported_operator (`Binop op, Ty_real)) in
+    let exact_op v1 v2 : Value.real = match op with
+      | Add -> Exact (Q.add v1 v2)
+      | Sub -> Exact (Q.sub v1 v2)
+      | Mul -> Exact (Q.mul v1 v2)
+      | Div -> Exact (Q.div v1 v2)
+      | Rem -> Exact (rem_q v1 v2)
+      | Min -> Exact (Q.min v1 v2)
+      | Max -> Exact (Q.max v1 v2)
+      | Pow -> Approx (Float.pow (Q.to_float v1) (Q.to_float v2))
+      | _ -> eval_error (`Unsupported_operator (`Binop op, Ty_real)) in
+    let push_approx_op (v1 : Value.real) (v2 : Value.real) =
+      match (v1, v2) with
+      | Exact v1, Exact v2 -> exact_op v1 v2
+      | Exact v1, Approx v2 -> approx_op (Q.to_float v1) v2
+      | Approx v1, Exact v2 -> approx_op v1 (Q.to_float v2)
+      | Approx v1, Approx v2 -> approx_op v1 v2 in
+    to_real (push_approx_op (of_real 1 (`Binop op) v1) (of_real 2 (`Binop op) v2))
 
   let relop (op : Ty.Relop.t) (v1 : Value.t) (v2 : Value.t) : bool =
-    let f =
-      match op with
+    let approx_op = match op with
       | Lt -> Float.Infix.( < )
       | Le -> Float.Infix.( <= )
       | Gt -> Float.Infix.( > )
       | Ge -> Float.Infix.( >= )
       | Eq -> Float.Infix.( = )
       | Ne -> Float.Infix.( <> )
-      | _ -> eval_error (`Unsupported_operator (`Relop op, Ty_real))
-    in
-    f (of_real 1 (`Relop op) v1) (of_real 2 (`Relop op) v2)
+      | _ -> eval_error (`Unsupported_operator (`Relop op, Ty_real)) in
+    let exact_op = match op with
+      | Lt -> Q.lt
+      | Le -> Q.leq
+      | Gt -> Q.gt
+      | Ge -> Q.geq
+      | Eq -> Q.equal
+      | Ne -> fun v1 v2 -> Fun.negate (Q.equal v1) v2
+      | _ -> eval_error (`Unsupported_operator (`Relop op, Ty_real)) in
+    let push_approx_op (v1 : Value.real) (v2 : Value.real) =
+      match (v1, v2) with
+      | Exact v1, Exact v2 -> exact_op v1 v2
+      | Exact v1, Approx v2 -> approx_op (Q.to_float v1) v2
+      | Approx v1, Exact v2 -> approx_op v1 (Q.to_float v2)
+      | Approx v1, Approx v2 -> approx_op v1 v2 in
+    push_approx_op (of_real 1 (`Relop op) v1) (of_real 2 (`Relop op) v2)
 
   let cvtop (op : Ty.Cvtop.t) (v : Value.t) : Value.t =
     let op' = `Cvtop op in
     match op with
-    | ToString -> Str (Float.to_string (of_real 1 op' v))
+    | ToString -> Str begin
+      match (of_real 1 op' v) with
+        | Exact v -> Q.to_string v
+        | Approx v -> Float.to_string v
+    end
     | OfString -> begin
-      match float_of_string_opt (of_str 1 op' v) with
-      | None -> eval_error `Invalid_format_conversion
-      | Some v -> to_real v
+      match (of_str 1 op' v) with
+        | float_str when String.contains float_str '.' -> begin
+          match (Float.of_string_opt float_str) with
+            | Some f -> to_real (Approx f)
+            | None -> eval_error `Invalid_format_conversion
+        end
+        | q_str -> begin
+          try to_real (Exact (Q.of_string q_str))
+          with | _ -> eval_error `Invalid_format_conversion
+        end
+    end
+    | Reinterpret_int -> to_real (Exact (Q.of_int @@ of_int 1 op' v))
+    | Reinterpret_float -> to_int begin
+      match (of_real 1 op' v) with
+        | Exact v -> Q.to_int v
+        | Approx v -> Float.to_int v
     end
-    | Reinterpret_int -> to_real (float_of_int (of_int 1 op' v))
-    | Reinterpret_float -> to_int (Float.to_int (of_real 1 op' v))
     | _ -> eval_error (`Unsupported_operator (op', Ty_real))
 end
 
@@ -408,7 +497,7 @@ module Str = struct
       let s = of_str 1 op' v in
       match float_of_string_opt s with
       | None -> eval_error `Invalid_format_conversion
-      | Some f -> to_real f
+      | Some f -> to_real (Approx f)
     end
     | _ -> eval_error (`Unsupported_operator (`Cvtop op, Ty_str))
 
diff --git a/src/smtml/eval.mli b/src/smtml/eval.mli
index 69d46cc1..45dc27d9 100644
--- a/src/smtml/eval.mli
+++ b/src/smtml/eval.mli
@@ -37,6 +37,7 @@ type error_kind =
   | `Integer_overflow
   | `Index_out_of_bounds
   | `Invalid_format_conversion
+  | `Negative_sqrt
   | `Unsupported_operator of op_type * Ty.t
   | `Unsupported_theory of Ty.t
   | `Type_error of type_error_info
diff --git a/src/smtml/expr.ml b/src/smtml/expr.ml
index cf66da75..e0669c2c 100644
--- a/src/smtml/expr.ml
+++ b/src/smtml/expr.ml
@@ -277,7 +277,7 @@ let normalize_eq_or_ne op (ty', e1, e2) =
       make_relop binop zero
     | Ty_real ->
       let binop = make (Binop (ty1, Sub, e1, e2)) in
-      let zero = make (Val (Real 0.)) in
+      let zero = make (Val (Real (Exact Q.zero))) in
       make_relop binop zero
     | _ -> make_relop e1 e2
   end
@@ -394,12 +394,18 @@ let raw_relop ty op hte1 hte2 = make (Relop (ty, op, hte1, hte2)) [@@inline]
 let rec relop ty op hte1 hte2 =
   match (op, view hte1, view hte2) with
   | op, Val v1, Val v2 -> value (if Eval.relop ty op v1 v2 then True else False)
-  | Ty.Relop.Ne, Val (Real v), _ | Ne, _, Val (Real v) ->
+  | Ty.Relop.Ne, Val (Real (Approx v)), _ | Ne, _, Val (Real (Approx v)) ->
     if Float.is_nan v || Float.is_infinite v then value True
     else raw_relop ty op hte1 hte2
-  | _, Val (Real v), _ | _, _, Val (Real v) ->
+  | Ty.Relop.Ne, Val (Real (Exact v)), _ | Ne, _, Val (Real (Exact v)) ->
+    if Fun.negate Q.is_real v then value True
+    else raw_relop ty op hte1 hte2
+  | _, Val (Real (Approx v)), _ | _, _, Val (Real (Approx v)) ->
     if Float.is_nan v || Float.is_infinite v then value False
     else raw_relop ty op hte1 hte2
+  | _, Val (Real (Exact v)), _ | _, _, Val (Real (Exact v)) ->
+    if Fun.negate Q.is_real v then value False
+    else raw_relop ty op hte1 hte2
   | Eq, _, Val Nothing | Eq, Val Nothing, _ -> value False
   | Ne, _, Val Nothing | Ne, Val Nothing, _ -> value True
   | Eq, _, Val (App (`Op "symbol", [ Str _ ]))
diff --git a/src/smtml/mappings.ml b/src/smtml/mappings.ml
index 8fe2ec46..87418000 100644
--- a/src/smtml/mappings.ml
+++ b/src/smtml/mappings.ml
@@ -162,8 +162,8 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
         let open M in
         match op with
         | Unop.Neg -> Real.neg e
-        | Abs -> ite (Real.gt e (real 0.)) e (Real.neg e)
-        | Sqrt -> Real.pow e (v 0.5)
+        | Abs -> ite (Real.gt e (real (Exact Q.zero))) e (Real.neg e)
+        | Sqrt -> Real.pow e (v (Exact (Q.make (Z.of_int 1) (Z.of_int 2))))
         | Ceil ->
           let x_int = M.Real.to_int e in
           ite (eq (Int.to_real x_int) e) x_int (Int.add x_int (int 1))
diff --git a/src/smtml/mappings_intf.ml b/src/smtml/mappings_intf.ml
index cc02d79f..0794ab14 100644
--- a/src/smtml/mappings_intf.ml
+++ b/src/smtml/mappings_intf.ml
@@ -47,7 +47,7 @@ module type M = sig
   val int : int -> term
 
   (** [real f] constructs a real number term from the given float [f]. *)
-  val real : float -> term
+  val real : Value.real -> term
 
   (** [const name ty] constructs a constant term with the given name and type.
   *)
@@ -143,7 +143,7 @@ module type M = sig
     val to_int : interp -> int
 
     (** [to_real interp] converts an interpretation to a real number. *)
-    val to_real : interp -> float
+    val to_real : interp -> Value.real
 
     (** [to_bool interp] converts an interpretation to a Boolean. *)
     val to_bool : interp -> bool
diff --git a/src/smtml/parser.mly b/src/smtml/parser.mly
index 27adddfd..3d5bb2c8 100644
--- a/src/smtml/parser.mly
+++ b/src/smtml/parser.mly
@@ -88,7 +88,7 @@ let paren_op :=
 
 let spec_constant :=
   | x = NUM; { Int x }
-  | x = DEC; { Real x }
+  | x = DEC; { Real (Approx x) }
   | x = STR; { Str x }
   | x = BOOL; { if x then True else False }
   | LPAREN; ty = TYPE; x = NUM; RPAREN;
diff --git a/src/smtml/smtlib.ml b/src/smtml/smtlib.ml
index a0db7ecf..71d1d036 100644
--- a/src/smtml/smtlib.ml
+++ b/src/smtml/smtlib.ml
@@ -107,9 +107,8 @@ module Term = struct
     | None -> Fmt.failwith "%ainvalid int" pp_loc loc
 
   let real ?loc (x : string) =
-    match float_of_string_opt x with
-    | Some x -> Expr.value (Real x)
-    | None -> Fmt.failwith "%ainvalid real" pp_loc loc
+    try Expr.value (Real (Exact (Q.of_string x)))
+    with | _ -> Fmt.failwith "%ainvalid real" pp_loc loc
 
   let hexa ?loc:_ (h : string) =
     let len = String.length h in
diff --git a/src/smtml/value.ml b/src/smtml/value.ml
index 215f85c0..2a540f4a 100644
--- a/src/smtml/value.ml
+++ b/src/smtml/value.ml
@@ -4,12 +4,14 @@
 
 open Ty
 
+type real = Exact of Q.t | Approx of float
+
 type t =
   | True
   | False
   | Unit
   | Int of int
-  | Real of float
+  | Real of real
   | Str of string
   | Num of Num.t
   | Bitv of Bitvector.t
@@ -49,7 +51,10 @@ let rec compare (a : t) (b : t) : int =
   | False, True -> -1
   | True, False -> 1
   | Int a, Int b -> Int.compare a b
-  | Real a, Real b -> Float.compare a b
+  | Real (Exact a), Real (Exact b) -> Q.compare a b
+  | Real (Approx a), Real (Approx b) -> Float.compare a b
+  | Real (Approx _), Real (Exact _) -> -1
+  | Real (Exact _), Real (Approx _) -> 1
   | Str a, Str b -> String.compare a b
   | Num a, Num b -> Num.compare a b
   | Bitv a, Bitv b -> Bitvector.compare a b
@@ -67,7 +72,9 @@ let rec equal (v1 : t) (v2 : t) : bool =
   match (v1, v2) with
   | True, True | False, False | Unit, Unit | Nothing, Nothing -> true
   | Int a, Int b -> Int.equal a b
-  | Real a, Real b -> Float.equal a b
+  | Real (Exact a), Real (Exact b) -> Q.equal a b
+  | Real (Approx a), Real (Approx b) -> Float.equal a b
+  | Real (Approx _), Real (Exact _) | Real (Exact _), Real (Approx _) -> false
   | Str a, Str b -> String.equal a b
   | Num a, Num b -> Num.equal a b
   | Bitv a, Bitv b -> Bitvector.equal a b
@@ -88,7 +95,8 @@ let rec pp fmt = function
   | False -> Fmt.string fmt "false"
   | Unit -> Fmt.string fmt "unit"
   | Int x -> Fmt.int fmt x
-  | Real x -> Fmt.pf fmt "%F" x
+  | Real (Exact x) -> Q.pp_print fmt x
+  | Real (Approx x) -> Fmt.pf fmt "%F" x
   | Num x -> Num.pp fmt x
   | Bitv bv -> Bitvector.pp fmt bv
   | Str x -> Fmt.pf fmt "%S" x
@@ -117,9 +125,8 @@ let of_string (cast : Ty.t) v =
     | None -> Fmt.error_msg "invalid value %s, expected integer" v
     | Some n -> Ok (Int n) )
   | Ty_real -> (
-    match float_of_string_opt v with
-    | None -> Fmt.error_msg "invalid value %s, expected real" v
-    | Some n -> Ok (Real n) )
+    try Ok (Real (Exact (Q.of_string v)))
+    with | _ -> Fmt.error_msg "invalid value %s, expected real" v)
   | Ty_str -> Ok (Str v)
   | Ty_app | Ty_list | Ty_none | Ty_unit | Ty_regexp | Ty_roundingMode ->
     Fmt.error_msg "unsupported parsing values of type %a" Ty.pp cast
@@ -130,7 +137,11 @@ let rec to_json (v : t) : Yojson.Basic.t =
   | False -> `Bool false
   | Unit -> `String "unit"
   | Int int -> `Int int
-  | Real real -> `Float real
+  | Real (Exact r) ->
+      let num = r |> Q.num |> Z.to_int in
+      let den = r |> Q.den |> Z.to_int in
+      `Assoc ["num", `Int num; "den", `Int den]
+  | Real (Approx r) -> `Float r
   | Str str -> `String str
   | Num n -> Num.to_json n
   | Bitv bv -> Bitvector.to_json bv
@@ -143,7 +154,8 @@ module Smtlib = struct
     | True -> Fmt.string fmt "true"
     | False -> Fmt.string fmt "false"
     | Int x -> Fmt.int fmt x
-    | Real x -> Fmt.pf fmt "%F" x
+    | Real (Exact x) -> Q.pp_print fmt x
+    | Real (Approx x) -> Fmt.pf fmt "%F" x
     | Num x -> Num.pp fmt x
     | Bitv bv -> Bitvector.pp fmt bv
     | Str x -> Fmt.pf fmt "%S" x
diff --git a/src/smtml/value.mli b/src/smtml/value.mli
index 71785473..681d34ab 100644
--- a/src/smtml/value.mli
+++ b/src/smtml/value.mli
@@ -9,13 +9,16 @@
 
 (** {1 Value Types} *)
 
+(** The type [real] represents either an exact rational, or an approximate float. *)
+type real = Exact of Q.t | Approx of float
+
 (** The type [t] represents concrete values. *)
 type t =
   | True  (** Boolean true. *)
   | False  (** Boolean false. *)
   | Unit  (** Unit value. *)
   | Int of int  (** Integer value. *)
-  | Real of float  (** Real number value. *)
+  | Real of real  (** Real number value. *)
   | Str of string  (** String value. *)
   | Num of Num.t  (** Numeric value. *)
   | Bitv of Bitvector.t  (** Bitvector value. *)
diff --git a/src/smtml/z3_mappings.default.ml b/src/smtml/z3_mappings.default.ml
index 4e78790e..198ca5f4 100644
--- a/src/smtml/z3_mappings.default.ml
+++ b/src/smtml/z3_mappings.default.ml
@@ -40,7 +40,11 @@ module M = struct
 
     let int i = Z3.Arithmetic.Integer.mk_numeral_i ctx i
 
-    let real f = Z3.Arithmetic.Real.mk_numeral_s ctx (Float.to_string f)
+    let real (f : Value.real) =
+      let str = match f with
+        | Exact q -> Q.to_string q
+        | Approx f -> Float.to_string f in
+      Z3.Arithmetic.Real.mk_numeral_s ctx str
 
     let const sym ty = Z3.Expr.mk_const_s ctx sym ty
 
@@ -108,7 +112,7 @@ module M = struct
     module Interp = struct
       let to_int interp = Z.to_int @@ Z3.Arithmetic.Integer.get_big_int interp
 
-      let to_real interp = Q.to_float @@ Z3.Arithmetic.Real.get_ratio interp
+      let to_real interp : Value.real = Exact (Z3.Arithmetic.Real.get_ratio interp)
 
       let to_bool interp =
         match Z3.Boolean.get_bool_value interp with
diff --git a/test/cli/smtml/test_smtml.t b/test/cli/smtml/test_smtml.t
index 79c3b360..8767a8ae 100644
--- a/test/cli/smtml/test_smtml.t
+++ b/test/cli/smtml/test_smtml.t
@@ -17,8 +17,8 @@ Test boolean parsing:
   $ smtml run test_lra.smtml
   sat
   (model
-    (x real 2.)
-    (y real 4.))
+    (x real 2)
+    (y real 4))
 
  Test fp parsing:
   $ smtml run test_qf_fp.smtml
diff --git a/test/unit/test_eval.ml b/test/unit/test_eval.ml
index 9b2db46d..0c62bacc 100644
--- a/test/unit/test_eval.ml
+++ b/test/unit/test_eval.ml
@@ -150,7 +150,7 @@ module Int_test = struct
       assert_equal (int 1) result
     in
     let test_reinterpret_float _ =
-      let result = Eval.cvtop Ty_int Reinterpret_float (real 42.0) in
+      let result = Eval.cvtop Ty_int Reinterpret_float (real (Approx 42.0)) in
       assert_equal (int 42) result
     in
     [ "test_of_bool" >:: test_of_bool
@@ -162,36 +162,57 @@ module Real_test = struct
   (* Unary operators *)
   let unop =
     let test_neg _ =
-      let result = Eval.unop Ty_real Neg (real 5.) in
-      assert_equal (real (-5.)) result
+      let result = Eval.unop Ty_real Neg (real (Approx 5.)) in
+      assert_equal (real (Approx (-5.))) result;
+      let result = Eval.unop Ty_real Neg (real (Exact (Q.of_int 5))) in
+      assert_equal (real (Exact (Q.neg @@ Q.of_int 5))) result
     in
     let test_abs _ =
-      let result = Eval.unop Ty_real Abs (real (-7.)) in
-      assert_equal (real 7.) result
+      let result = Eval.unop Ty_real Abs (real (Approx (-7.))) in
+      assert_equal (real (Approx 7.)) result;
+      let result = Eval.unop Ty_real Abs (real (Exact (Q.neg @@ Q.of_int 7))) in
+      assert_equal (real (Exact (Q.of_int 7))) result;
+      let result = Eval.unop Ty_real Abs (real (Exact (Q.neg @@ Q.of_string "5/2"))) in
+      assert_equal (real (Exact (Q.of_string "5/2"))) result
     in
     let test_sqrt _ =
-      let result = Eval.unop Ty_real Sqrt (real 9.) in
-      assert_equal (real 3.) result
+      let result = Eval.unop Ty_real Sqrt (real (Approx 9.0)) in
+      assert_equal (real (Approx 3.)) result;
+      let result = Eval.unop Ty_real Sqrt (real (Exact (Q.of_int 9))) in
+      assert_equal (real (Exact (Q.of_int 3))) result;
+      let result = Eval.unop Ty_real Sqrt (real (Exact (Q.of_string "25/4"))) in
+      assert_equal (real (Exact (Q.of_string "5/2"))) result
     in
     let test_nearest _ =
-      assert_equal (real 4.) (Eval.unop Ty_real Nearest (real 4.2));
-      assert_equal (real 5.) (Eval.unop Ty_real Nearest (real 4.6))
+      assert_equal (real (Approx 4.)) (Eval.unop Ty_real Nearest (real (Approx 4.2)));
+      assert_equal (real (Exact (Q.of_int 4))) (Eval.unop Ty_real Nearest (real (Exact (Q.of_float 4.2))));
+      assert_equal (real (Approx 5.)) (Eval.unop Ty_real Nearest (real (Approx 4.6)));
+      assert_equal (real (Exact (Q.of_float 5.))) (Eval.unop Ty_real Nearest (real (Exact (Q.of_float 4.6))))
     in
     let test_ceil _ =
-      let result = Eval.unop Ty_real Ceil (real 4.2) in
-      assert_equal (real 5.) result
+      let result = Eval.unop Ty_real Ceil (real (Approx 4.2)) in
+      assert_equal (real (Approx 5.)) result;
+      let result = Eval.unop Ty_real Ceil (real (Exact (Q.of_float 4.2))) in
+      assert_equal (real (Exact (Q.of_float 5.))) result
     in
     let test_floor _ =
-      let result = Eval.unop Ty_real Floor (real 4.2) in
-      assert_equal (real 4.) result
+      let result = Eval.unop Ty_real Floor (real (Approx 4.2)) in
+      assert_equal (real (Approx 4.)) result;
+      let result = Eval.unop Ty_real Floor (real (Exact (Q.of_float 4.2))) in
+      assert_equal (real (Exact (Q.of_float 4.2))) result
     in
     let test_trunc _ =
-      let result = Eval.unop Ty_real Trunc (real Float.pi) in
-      assert_equal (real 3.) result
+      let result = Eval.unop Ty_real Trunc (real (Approx Float.pi)) in
+      assert_equal (real (Approx 3.)) result;
+      let result = Eval.unop Ty_real Trunc (real (Exact (Q.of_string "3.141592"))) in
+      assert_equal (real (Exact (Q.of_int 3))) result
+
     in
     let test_is_nan _ =
-      assert_equal (Eval.unop Ty_real Is_nan (real Float.nan)) true_;
-      assert_equal (Eval.unop Ty_real Is_nan (real 42.)) false_
+      assert_equal (Eval.unop Ty_real Is_nan (real (Approx Float.nan))) true_;
+      assert_equal (Eval.unop Ty_real Is_nan (real (Exact Q.undef))) true_;
+      assert_equal (Eval.unop Ty_real Is_nan (real (Approx 42.))) false_;
+      assert_equal (Eval.unop Ty_real Is_nan (real (Exact (Q.of_int 4)))) false_
     in
     let test_type_error _ =
       assert_type_error @@ fun () -> ignore @@ Eval.unop Ty_real Neg (str "hi")
@@ -209,6 +230,7 @@ module Real_test = struct
 
   (* Binary operators *)
   let binop =
+    let real r = real (Approx r) in
     let test_add _ =
       let result = Eval.binop Ty_real Add (real 2.) (real 3.) in
       assert_equal (real 5.) result
@@ -257,6 +279,7 @@ module Real_test = struct
 
   (* Relational operators *)
   let relop =
+    let real r = real (Approx r) in
     let test_eq _ =
       assert_bool "0 = 0" (Eval.relop Ty_real Eq (real 0.0) (real 0.0));
       assert_bool "nan != nan"
@@ -292,11 +315,15 @@ module Real_test = struct
   let cvtop =
     let test_of_string _ =
       let result = Eval.cvtop Ty_real OfString (str "42.") in
-      assert_equal (real 42.) result
+      assert_equal (real (Approx 42.)) result;
+      let result = Eval.cvtop Ty_real OfString (str "42") in
+      assert_equal (real (Exact (Q.of_int 42))) result
     in
     let test_to_string _ =
-      let result = Eval.cvtop Ty_real ToString (real 42.) in
-      assert_equal (str "42.") result
+      let result = Eval.cvtop Ty_real ToString (real (Approx 42.)) in
+      assert_equal (str "42.") result;
+      let result = Eval.cvtop Ty_real ToString (real (Exact (Q.of_int 42))) in
+      assert_equal (str "42") result
     in
     let test_of_string_error _ =
       assert_raises (Eval.Eval_error `Invalid_format_conversion) @@ fun () ->
@@ -305,10 +332,10 @@ module Real_test = struct
     in
     let test_reinterpret_int _ =
       let result = Eval.cvtop Ty_real Reinterpret_int (int 42) in
-      assert_equal (real 42.) result
+      assert_equal (real (Exact (Q.of_int 42))) result
     in
     let test_reinterpret_float _ =
-      let result = Eval.cvtop Ty_real Reinterpret_float (real 42.) in
+      let result = Eval.cvtop Ty_real Reinterpret_float (real (Approx 42.)) in
       assert_equal (int 42) result
     in
     [ "test_to_string" >:: test_to_string
@@ -471,7 +498,7 @@ module Str_test = struct
         assert_equal (str "97") result )
     ; ( "test_string_to_float" >:: fun _ ->
         let result = Eval.cvtop Ty_str String_to_float (str "98") in
-        assert_equal (real 98.) result )
+        assert_equal (real (Approx 98.)) result )
     ; ( "test_string_to_float_raises" >:: fun _ ->
         assert_raises (Eval.Eval_error `Invalid_format_conversion) @@ fun () ->
         let _ = Eval.cvtop Ty_str String_to_float (str "not_a_real") in
diff --git a/test/unit/test_expr.ml b/test/unit/test_expr.ml
index 2f4f62f5..45706587 100644
--- a/test/unit/test_expr.ml
+++ b/test/unit/test_expr.ml
@@ -44,9 +44,10 @@ let test_unop_int _ =
   let x = symbol "x" ty in
   check (Expr.unop ty Neg (Expr.unop ty Neg x)) x
 
-let test_unop_real _ =
+let test_unop_real_approx _ =
   let open Infix in
   let ty = Ty.Ty_real in
+  let real r = real (Approx r) in
   check (Expr.unop ty Neg (real 1.0)) (real (-1.0));
   check (Expr.unop ty Abs (real 1.0)) (real 1.0);
   check (Expr.unop ty Sqrt (real 4.0)) (real 2.0);
@@ -56,6 +57,20 @@ let test_unop_real _ =
   check (Expr.unop ty Trunc (real 1.504)) (real 1.0);
   check (Expr.unop ty Is_nan (real Float.nan)) true_
 
+let test_unop_real_exact _ =
+  let open Infix in
+  let ty = Ty.Ty_real in
+  let real r = real (Exact r) in
+  let open Q in
+  check (Expr.unop ty Neg (real one)) (real (neg one));
+  check (Expr.unop ty Abs (real one)) (real one);
+  check (Expr.unop ty Sqrt (real (of_int 4))) (real (of_int 2));
+  check (Expr.unop ty Nearest (real (of_float 0.504))) (real one);
+  check (Expr.unop ty Ceil (real (of_float 0.3))) (real one);
+  check (Expr.unop ty Floor (real (of_float 0.7))) (real zero);
+  check (Expr.unop ty Trunc (real (of_float 1.504))) (real one);
+  check (Expr.unop ty Is_nan (real Q.undef)) true_
+
 let test_unop_string _ =
   let open Infix in
   let ty = Ty.Ty_str in
@@ -110,7 +125,8 @@ let test_unop_f64 _ =
 
 let test_unop =
   [ "test_unop_int" >:: test_unop_int
-  ; "test_unop_real" >:: test_unop_real
+  ; "test_unop_real_exact" >:: test_unop_real_exact
+  ; "test_unop_real_approx" >:: test_unop_real_approx
   ; "test_unop_stri" >:: test_unop_string
   ; "test_unop_bool" >:: test_unop_bool
   ; "test_unop_list" >:: test_unop_list
@@ -139,9 +155,10 @@ let test_binop_int _ =
   check (Expr.binop ty ShrA (int (-4)) (int 2)) (int (-1))
 (* check (Expr.binop ty ShrL (int (-4)) (int 2)) (int (-1)) *)
 
-let test_binop_real _ =
+let test_binop_real_approx _ =
   let open Infix in
   let ty = Ty.Ty_real in
+  let real r = real (Approx r) in
   check (Expr.binop ty Add (real 0.0) (real 42.0)) (real 42.0);
   check (Expr.binop ty Sub (real 0.0) (real 1.0)) (real (-1.0));
   check (Expr.binop ty Mul (real 2.0) (real 21.0)) (real 42.0);
@@ -150,6 +167,22 @@ let test_binop_real _ =
   check (Expr.binop ty Min (real 2.0) (real 4.0)) (real 2.0);
   check (Expr.binop ty Max (real 2.0) (real 4.0)) (real 4.0)
 
+let test_binop_real_exact _ =
+  let open Infix in
+  let ty = Ty.Ty_real in
+  let real r = real (Exact r) in
+  let open Q in
+  check (Expr.binop ty Add (real zero) (real (of_int 42))) (real (of_int 42));
+  check (Expr.binop ty Add (real (of_string "2/3")) (real (of_string "1/3"))) (real one);
+  check (Expr.binop ty Sub (real zero) (real one)) (real (neg one));
+  check (Expr.binop ty Mul (real (of_int 2)) (real (of_int 21))) (real (of_int 42));
+  check (Expr.binop ty Mul (real (of_string "1/3")) (real (of_int 2))) (real (of_string "2/3"));
+  check (Expr.binop ty Div (real (of_int 84)) (real (of_int 2))) (real (of_int 42));
+  check (Expr.binop ty Rem (real zero) (real one)) (real zero);
+  check (Expr.binop ty Min (real (of_int 2)) (real (of_int 4))) (real (of_int 2));
+  check (Expr.binop ty Max (real (of_int 2)) (real (of_int 4))) (real (of_int 4))
+
+
 let test_binop_string _ =
   let open Infix in
   let ty = Ty.Ty_str in
@@ -261,7 +294,8 @@ let test_binop_simplifications _ =
 
 let test_binop =
   [ "test_binop_int" >:: test_binop_int
-  ; "test_binop_real" >:: test_binop_real
+  ; "test_binop_real_exact" >:: test_binop_real_exact
+  ; "test_binop_real_approx" >:: test_binop_real_approx
   ; "test_binop_string" >:: test_binop_string
   ; "test_binop_list" >:: test_binop_list
   ; "test_binop_i32" >:: test_binop_i32
@@ -277,8 +311,8 @@ let test_relop_bool _ =
   let ty = Ty.Ty_bool in
   check (Expr.relop ty Eq (int 0) (int 0)) true_;
   check (Expr.relop ty Ne (int 0) (int 0)) false_;
-  check (Expr.relop ty Eq (real 0.0) (real 0.0)) true_;
-  check (Expr.relop ty Ne (real 0.0) (real 0.0)) false_;
+  check (Expr.relop ty Eq (real (Exact Q.zero)) (real (Exact Q.zero))) true_;
+  check (Expr.relop ty Ne (real (Exact Q.zero)) (real (Exact Q.zero))) false_;
   check (Expr.relop ty Eq (int32 0l) (int32 0l)) true_;
   check (Expr.relop ty Ne (int32 0l) (int32 0l)) false_;
   check (Expr.relop ty Eq (int64 0L) (int64 0L)) true_;
@@ -292,10 +326,11 @@ let test_relop_int _ =
   check (Expr.relop ty Gt (int 0) (int 1)) false_;
   check (Expr.relop ty Ge (int 0) (int 1)) false_
 
-let test_relop_real _ =
+let test_relop_real_approx _ =
   let open Infix in
   let ty = Ty.Ty_real in
   let x = symbol "x" ty in
+  let real r = real (Approx r) in
   check (Expr.relop Ty_bool Ne (real Float.nan) x) true_;
   check (Expr.relop Ty_bool Eq x (real Float.nan)) false_;
   check (Expr.relop ty Lt (real 0.0) (real 1.0)) true_;
@@ -303,6 +338,19 @@ let test_relop_real _ =
   check (Expr.relop ty Gt (real 0.0) (real 1.0)) false_;
   check (Expr.relop ty Ge (real 0.0) (real 1.0)) false_
 
+let test_relop_real_exact _ =
+  let open Infix in
+  let ty = Ty.Ty_real in
+  let x = symbol "x" ty in
+  let real r = real (Exact r) in
+  let open Q in
+  check (Expr.relop Ty_bool Ne (real Q.undef) x) true_;
+  check (Expr.relop Ty_bool Eq x (real Q.undef)) false_;
+  check (Expr.relop ty Lt (real zero) (real one)) true_;
+  check (Expr.relop ty Le (real zero) (real one)) true_;
+  check (Expr.relop ty Gt (real zero) (real one)) false_;
+  check (Expr.relop ty Ge (real zero) (real one)) false_
+
 let test_relop_string _ =
   let open Infix in
   let ty = Ty.Ty_str in
@@ -398,7 +446,8 @@ let test_relop_eq _ =
 let test_relop =
   [ "test_relop_bool" >:: test_relop_bool
   ; "test_relop_int" >:: test_relop_int
-  ; "test_relop_real" >:: test_relop_real
+  ; "test_relop_real_exact" >:: test_relop_real_exact
+  ; "test_relop_real_approx" >:: test_relop_real_approx
   ; "test_relop_string" >:: test_relop_string
   ; "test_relop_i32" >:: test_relop_i32
   ; "test_relop_i64" >:: test_relop_i64
@@ -446,14 +495,16 @@ let test_cvtop_int _ =
   let ty = Ty.Ty_int in
   check (Expr.cvtop ty OfBool true_) (int 1);
   check (Expr.cvtop ty OfBool false_) (int 0);
-  check (Expr.cvtop ty Reinterpret_float (real 1.)) (int 1)
+  check (Expr.cvtop ty Reinterpret_float (real (Exact Q.one))) (int 1)
 
 let test_cvtop_real _ =
   let open Infix in
   let ty = Ty.Ty_real in
-  check (Expr.cvtop ty ToString (real 1.)) (string "1.");
-  check (Expr.cvtop ty OfString (string "1.")) (real 1.);
-  check (Expr.cvtop ty Reinterpret_int (int 1)) (real 1.)
+  check (Expr.cvtop ty ToString (real (Exact Q.one))) (string "1");
+  check (Expr.cvtop ty ToString (real (Approx 1.))) (string "1.");
+  check (Expr.cvtop ty OfString (string "1.")) (real (Approx 1.));
+  check (Expr.cvtop ty OfString (string "1")) (real (Exact Q.one));
+  check (Expr.cvtop ty Reinterpret_int (int 1)) (real (Exact Q.one))
 
 let test_cvtop_string _ =
   let open Infix in
@@ -462,7 +513,8 @@ let test_cvtop_string _ =
   check (Expr.cvtop ty String_from_code (int 97)) (string "a");
   check (Expr.cvtop ty String_to_int (string "42")) (int 42);
   check (Expr.cvtop ty String_from_int (int 42)) (string "42");
-  check (Expr.cvtop ty String_to_float (string "1.")) (real 1.)
+  check (Expr.cvtop ty String_to_float (string "1.")) (real (Approx 1.));
+  check (Expr.cvtop ty String_to_float (string "1")) (real (Approx 1.))
 
 let test_cvtop_i32 _ =
   let open Infix in
diff --git a/test/unit/test_model.ml b/test/unit/test_model.ml
index 41d99b6a..36fea530 100644
--- a/test/unit/test_model.ml
+++ b/test/unit/test_model.ml
@@ -26,7 +26,7 @@ let test_to_json _ =
     let tbl = Hashtbl.create 16 in
     List.iter
       (fun ((s, v) : Symbol.t * Value.t) -> Hashtbl.replace tbl s v)
-      [ (x, Int 1); (y, Real 2.0); (z, True); (u, Str "abc") ];
+      [ (x, Int 1); (y, Real (Approx 2.0)); (z, True); (u, Str "abc") ];
     tbl
   in
   let model_to_json = Model.to_json model in

From 43397a7f9486083a7c63ef5f0d4972b56dbc9ab8 Mon Sep 17 00:00:00 2001
From: Tiago Ferreira <me@tiferrei.com>
Date: Tue, 9 Dec 2025 19:13:32 +0000
Subject: [PATCH 2/5] test: Exact reals in binop tests.

---
 test/unit/test_eval.ml | 93 ++++++++++++++++++++++++++++++------------
 1 file changed, 66 insertions(+), 27 deletions(-)

diff --git a/test/unit/test_eval.ml b/test/unit/test_eval.ml
index 0c62bacc..b3b46cf8 100644
--- a/test/unit/test_eval.ml
+++ b/test/unit/test_eval.ml
@@ -185,21 +185,21 @@ module Real_test = struct
     in
     let test_nearest _ =
       assert_equal (real (Approx 4.)) (Eval.unop Ty_real Nearest (real (Approx 4.2)));
-      assert_equal (real (Exact (Q.of_int 4))) (Eval.unop Ty_real Nearest (real (Exact (Q.of_float 4.2))));
+      assert_equal (real (Exact (Q.of_int 4))) (Eval.unop Ty_real Nearest (real (Exact (Q.of_string "42/10"))));
       assert_equal (real (Approx 5.)) (Eval.unop Ty_real Nearest (real (Approx 4.6)));
-      assert_equal (real (Exact (Q.of_float 5.))) (Eval.unop Ty_real Nearest (real (Exact (Q.of_float 4.6))))
+      assert_equal (real (Exact (Q.of_int 5))) (Eval.unop Ty_real Nearest (real (Exact (Q.of_string "46/10"))))
     in
     let test_ceil _ =
       let result = Eval.unop Ty_real Ceil (real (Approx 4.2)) in
       assert_equal (real (Approx 5.)) result;
-      let result = Eval.unop Ty_real Ceil (real (Exact (Q.of_float 4.2))) in
-      assert_equal (real (Exact (Q.of_float 5.))) result
+      let result = Eval.unop Ty_real Ceil (real (Exact (Q.of_string "42/10"))) in
+      assert_equal (real (Exact (Q.of_int 5))) result
     in
     let test_floor _ =
       let result = Eval.unop Ty_real Floor (real (Approx 4.2)) in
       assert_equal (real (Approx 4.)) result;
-      let result = Eval.unop Ty_real Floor (real (Exact (Q.of_float 4.2))) in
-      assert_equal (real (Exact (Q.of_float 4.2))) result
+      let result = Eval.unop Ty_real Floor (real (Exact (Q.of_string "42/10"))) in
+      assert_equal (real (Exact (Q.of_int 4))) result
     in
     let test_trunc _ =
       let result = Eval.unop Ty_real Trunc (real (Approx Float.pi)) in
@@ -230,42 +230,81 @@ module Real_test = struct
 
   (* Binary operators *)
   let binop =
-    let real r = real (Approx r) in
     let test_add _ =
-      let result = Eval.binop Ty_real Add (real 2.) (real 3.) in
-      assert_equal (real 5.) result
+      let result = Eval.binop Ty_real Add (real (Approx 2.)) (real (Approx 3.)) in
+      assert_equal (real (Approx 5.)) result;
+      let result = Eval.binop Ty_real Add (real (Exact (Q.of_int 2))) (real (Exact (Q.of_int 3))) in
+      assert_equal (real (Exact (Q.of_int 5))) result;
+      let result = Eval.binop Ty_real Add (real (Exact (Q.of_string "2/3"))) (real (Exact (Q.of_string "1/3"))) in
+      assert_equal (real (Exact (Q.one))) result
     in
     let test_sub _ =
-      let result = Eval.binop Ty_real Sub (real 3.) (real 2.) in
-      assert_equal (real 1.) result
+      let result = Eval.binop Ty_real Sub (real (Approx 3.)) (real (Approx 2.)) in
+      assert_equal (real (Approx 1.)) result;
+      let result = Eval.binop Ty_real Sub (real (Exact (Q.of_int 3))) (real (Exact (Q.of_int 2))) in
+      assert_equal (real (Exact Q.one)) result;
+      let result = Eval.binop Ty_real Sub (real (Exact (Q.of_int 1))) (real (Exact (Q.of_string "1/3"))) in
+      assert_equal (real (Exact (Q.of_string "2/3"))) result
     in
     let test_mul _ =
-      let result = Eval.binop Ty_real Mul (real 3.) (real 3.) in
-      assert_equal (real 9.) result
+      let result = Eval.binop Ty_real Mul (real (Approx 3.)) (real (Approx 3.)) in
+      assert_equal (real (Approx 9.)) result;
+      let result = Eval.binop Ty_real Mul (real (Exact (Q.of_int 3))) (real (Exact (Q.of_int 3))) in
+      assert_equal (real (Exact (Q.of_int 9))) result;
+      let result = Eval.binop Ty_real Mul (real (Exact (Q.of_string "2/3"))) (real (Exact (Q.of_int 2))) in
+      assert_equal (real (Exact (Q.of_string "4/3"))) result
     in
     let test_div _ =
-      let result = Eval.binop Ty_real Div (real 6.) (real 3.) in
-      assert_equal (real 2.) result
+      let result = Eval.binop Ty_real Div (real (Approx 6.)) (real (Approx 3.)) in
+      assert_equal (real (Approx 2.)) result;
+      let result = Eval.binop Ty_real Div (real (Exact (Q.of_int 6))) (real (Exact (Q.of_int 3))) in
+      assert_equal (real (Exact (Q.of_int 2))) result;
+      let result = Eval.binop Ty_real Div (real (Exact (Q.of_string "4/3"))) (real (Exact (Q.of_int 2))) in
+      assert_equal (real (Exact (Q.of_string "2/3"))) result
     in
     let test_divide_by_zero _ =
-      let result = Eval.binop Ty_real Div (real 1.) (real 0.) in
-      assert_equal (real Float.infinity) result
+      let result = Eval.binop Ty_real Div (real (Approx 1.)) (real (Approx 0.)) in
+      assert_equal (real (Approx Float.infinity)) result;
+      let result = Eval.binop Ty_real Div (real (Exact Q.one)) (real (Exact Q.zero)) in
+      assert_equal (real (Exact Q.inf)) result;
+      let result = Eval.binop Ty_real Div (real (Exact (Q.of_string "2/3"))) (real (Exact (Q.of_string "0/5"))) in
+      assert_equal (real (Exact Q.inf)) result
     in
     let test_rem _ =
-      let result = Eval.binop Ty_real Rem (real 6.) (real 3.) in
-      assert_equal (real 0.) result
+      let result = Eval.binop Ty_real Rem (real (Approx 6.)) (real (Approx 3.)) in
+      assert_equal (real (Approx 0.)) result;
+      let result = Eval.binop Ty_real Rem (real (Exact (Q.of_int 6))) (real (Exact (Q.of_int 3))) in
+      assert_equal (real (Exact Q.zero)) result;
+      let result = Eval.binop Ty_real Rem (real (Exact (Q.of_string "7/3"))) (real (Exact (Q.of_string "2/3"))) in
+      assert_equal (real (Exact (Q.of_string "1/3"))) result;
+      let result = Eval.binop Ty_real Rem (real (Exact (Q.of_string "-7/3"))) (real (Exact (Q.of_string "2/3"))) in
+      assert_equal (real (Exact (Q.of_string "-1/3"))) result;
+      let result = Eval.binop Ty_real Rem (real (Exact (Q.of_string "5/2"))) (real (Exact (Q.of_string "1/2"))) in
+      assert_equal (real (Exact (Q.of_string "0/1"))) result;
+      let result = Eval.binop Ty_real Rem (real (Exact (Q.of_string "5/2"))) (real (Exact (Q.of_string "1/3"))) in
+      assert_equal (real (Exact (Q.of_string "1/6"))) result;
+      let result = Eval.binop Ty_real Rem (real (Exact (Q.of_string "-5/2"))) (real (Exact (Q.of_string "1/3"))) in
+      assert_equal (real (Exact (Q.of_string "-1/6"))) result
     in
     let test_pow _ =
-      let result = Eval.binop Ty_real Pow (real 2.) (real 3.) in
-      assert_equal (real 8.) result
+      let result = Eval.binop Ty_real Pow (real (Approx 2.)) (real (Approx 3.)) in
+      assert_equal (real (Approx 8.)) result;
+      let result = Eval.binop Ty_real Pow (real (Exact (Q.of_int 2))) (real (Exact (Q.of_int 3))) in
+      assert_equal (real (Approx 8.)) result
     in
     let test_min_max _ =
-      let a = real 42. in
-      let b = real 1337. in
-      let result = Eval.binop Ty_real Max a b in
-      assert_equal (real 1337.) result;
-      let result = Eval.binop Ty_real Min a b in
-      assert_equal (real 42.) result
+      let a_f = real (Approx 42.) in
+      let b_f = real (Approx 1337.) in
+      let a_q = real (Exact (Q.of_int 42)) in
+      let b_q = real (Exact (Q.of_int 1337)) in
+      let result = Eval.binop Ty_real Max a_f b_f in
+      assert_equal b_f result;
+      let result = Eval.binop Ty_real Max a_q b_q in
+      assert_equal b_q result;
+      let result = Eval.binop Ty_real Min a_f b_f in
+      assert_equal a_f result;
+      let result = Eval.binop Ty_real Min a_q b_q in
+      assert_equal a_q result
     in
     [ "test_add" >:: test_add
     ; "test_sub" >:: test_sub

From 273d7626e3046a29557646c791ab128139ba406e Mon Sep 17 00:00:00 2001
From: Tiago Ferreira <me@tiferrei.com>
Date: Tue, 9 Dec 2025 19:27:16 +0000
Subject: [PATCH 3/5] test: Exact reals in relop tests.

---
 test/unit/test_eval.ml | 31 ++++++++++++++++++++++---------
 1 file changed, 22 insertions(+), 9 deletions(-)

diff --git a/test/unit/test_eval.ml b/test/unit/test_eval.ml
index b3b46cf8..f9b6664a 100644
--- a/test/unit/test_eval.ml
+++ b/test/unit/test_eval.ml
@@ -318,28 +318,41 @@ module Real_test = struct
 
   (* Relational operators *)
   let relop =
-    let real r = real (Approx r) in
     let test_eq _ =
-      assert_bool "0 = 0" (Eval.relop Ty_real Eq (real 0.0) (real 0.0));
+      assert_bool "0.0 = 0.0" (Eval.relop Ty_real Eq (real (Approx 0.0)) (real (Approx 0.0)));
+      assert_bool "0 = 0" (Eval.relop Ty_real Eq (real (Exact Q.zero)) (real (Exact Q.zero)));
       assert_bool "nan != nan"
-        (not (Eval.relop Ty_real Eq (real Float.nan) (real Float.nan)))
+        (not (Eval.relop Ty_real Eq (real (Approx Float.nan)) (real (Approx Float.nan))));
+      assert_bool "undef != undef"
+        (not (Eval.relop Ty_real Eq (real (Exact Q.undef)) (real (Exact Q.undef))))
     in
     let test_ne _ =
-      assert_bool "0 = 0" (not (Eval.relop Ty_real Ne (real 0.0) (real 0.0)));
+      assert_bool "0.0 = 0.0" (not (Eval.relop Ty_real Ne (real (Approx 0.0)) (real (Approx 0.0))));
+      assert_bool "0 = 0" (not (Eval.relop Ty_real Ne (real (Exact Q.zero)) (real (Exact Q.zero))));
       assert_bool "nan != nan"
-        (Eval.relop Ty_real Ne (real Float.nan) (real Float.nan))
+        (Eval.relop Ty_real Ne (real (Approx Float.nan)) (real (Approx Float.nan)));
+      assert_bool "undef != undef"
+        (Eval.relop Ty_real Ne (real (Exact Q.undef)) (real (Exact Q.undef)))
     in
     let test_lt _ =
-      assert_bool "2 < 3" (Eval.relop Ty_real Lt (real 2.) (real 3.))
+      assert_bool "2.0 < 3.0" (Eval.relop Ty_real Lt (real (Approx 2.)) (real (Approx 3.)));
+      assert_bool "2 < 3" (Eval.relop Ty_real Lt (real (Exact (Q.of_int 2))) (real (Exact (Q.of_int 3))));
+      assert_bool "2/3 < 3/3" (Eval.relop Ty_real Lt (real (Exact (Q.of_string "2/3"))) (real (Exact (Q.of_string "3/3"))))
     in
     let test_le _ =
-      assert_bool "2 <= 3" (Eval.relop Ty_real Le (real 3.) (real 3.))
+      assert_bool "2.0 <= 3.0" (Eval.relop Ty_real Le (real (Approx 2.)) (real (Approx 3.)));
+      assert_bool "2 <= 3" (Eval.relop Ty_real Le (real (Exact (Q.of_int 2))) (real (Exact (Q.of_int 3))));
+      assert_bool "2/3 <= 3/3" (Eval.relop Ty_real Le (real (Exact (Q.of_string "2/3"))) (real (Exact (Q.of_string "3/3"))))
     in
     let test_gt _ =
-      assert_bool "4 > 4" (Eval.relop Ty_real Gt (real 4.) (real 3.))
+      assert_bool "4.0 > 3.0" (Eval.relop Ty_real Gt (real (Approx 4.)) (real (Approx 3.)));
+      assert_bool "4 > 3" (Eval.relop Ty_real Gt (real (Exact (Q.of_int 4))) (real (Exact (Q.of_int 3))));
+      assert_bool "1/3 > 1/4" (Eval.relop Ty_real Gt (real (Exact (Q.of_string "1/3"))) (real (Exact (Q.of_string "1/4"))))
     in
     let test_ge _ =
-      assert_bool "4 >= 4" (Eval.relop Ty_real Ge (real 4.) (real 4.))
+      assert_bool "4.0 >= 3.0" (Eval.relop Ty_real Ge (real (Approx 4.)) (real (Approx 3.)));
+      assert_bool "4 >= 3" (Eval.relop Ty_real Ge (real (Exact (Q.of_int 4))) (real (Exact (Q.of_int 3))));
+      assert_bool "1/3 >= 1/4" (Eval.relop Ty_real Ge (real (Exact (Q.of_string "1/3"))) (real (Exact (Q.of_string "1/4"))))
     in
 
     [ "test_eq" >:: test_eq

From 5ccdd836dbfa1b3caf53b692a2abc01d79316902 Mon Sep 17 00:00:00 2001
From: Tiago Ferreira <me@tiferrei.com>
Date: Tue, 9 Dec 2025 19:33:13 +0000
Subject: [PATCH 4/5] fix: test_smt2.t

---
 test/cli/smt2/test_smt2.t | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/test/cli/smt2/test_smt2.t b/test/cli/smt2/test_smt2.t
index 143b3660..b78f8ae9 100644
--- a/test/cli/smt2/test_smt2.t
+++ b/test/cli/smt2/test_smt2.t
@@ -33,8 +33,8 @@ Test Real parsing:
   $ smtml run test_lra.smt2
   sat
   (model
-    (x real 2.)
-    (y real 4.))
+    (x real 2)
+    (y real 4))
 
 Test String parsing:
   $ smtml run test_string_all.smt2
@@ -88,8 +88,8 @@ Tests smt2 with the --from-file argument:
   sat
   sat
   (model
-    (x real 2.)
-    (y real 4.))
+    (x real 2)
+    (y real 4))
   sat
   sat
   (model
@@ -117,7 +117,7 @@ Test status tracking:
   sat
   smtml: internal error, uncaught exception:
          Failure("Expected status: unsat, but solver returned sat")
-         
+
   [125]
 
   $ smtml run --no-strict-status test_set_info_status.smt2

From c207145d28ed9f2409224fae41b1301e9140e65e Mon Sep 17 00:00:00 2001
From: Tiago Ferreira <me@tiferrei.com>
Date: Tue, 9 Dec 2025 19:40:06 +0000
Subject: [PATCH 5/5] fix: formatting

---
 src/smtml/eval.ml                | 121 +++++++++-------
 src/smtml/expr.ml                |   6 +-
 src/smtml/smtlib.ml              |   2 +-
 src/smtml/value.ml               |  12 +-
 src/smtml/value.mli              |   7 +-
 src/smtml/z3_mappings.default.ml |   9 +-
 test/unit/test_eval.ml           | 236 ++++++++++++++++++++++++-------
 test/unit/test_expr.ml           |  25 +++-
 8 files changed, 290 insertions(+), 128 deletions(-)

diff --git a/src/smtml/eval.ml b/src/smtml/eval.ml
index b668f05c..4b2a5d12 100644
--- a/src/smtml/eval.ml
+++ b/src/smtml/eval.ml
@@ -195,11 +195,12 @@ module Int = struct
   let cvtop (op : Ty.Cvtop.t) (v : Value.t) : Value.t =
     match op with
     | OfBool -> to_int (of_bool v)
-    | Reinterpret_float -> Int begin
-      match (of_real 1 (`Cvtop op) v) with
+    | Reinterpret_float ->
+      Int
+        begin match of_real 1 (`Cvtop op) v with
         | Exact v -> Q.to_int v
         | Approx v -> Int.of_float v
-    end
+        end
     | _ -> eval_error (`Unsupported_operator (`Cvtop op, Ty_int))
 end
 
@@ -209,23 +210,25 @@ module Real = struct
     let sqrt_q (q : Q.t) =
       let n = Q.num q in
       let d = Q.den q in
-      if Z.sign n < 0
-        then eval_error (`Negative_sqrt)
+      if Z.sign n < 0 then eval_error `Negative_sqrt
       else
-        let (n_root, n_rem) = Z.sqrt_rem n in
-        let (d_root, d_rem) = Z.sqrt_rem d in
+        let n_root, n_rem = Z.sqrt_rem n in
+        let d_root, d_rem = Z.sqrt_rem d in
         if Z.equal n_rem Z.zero && Z.equal d_rem Z.zero then
           to_real (Exact (Q.make n_root d_root))
-        else
-          to_real (Approx (Q.to_float q |> sqrt)) in
+        else to_real (Approx (Q.to_float q |> sqrt))
+    in
     let nearest_q (q : Q.t) =
       let n = Q.num q in
       let d = Q.den q in
-      let near = if Z.geq n Z.zero
-        then Z.div (Z.add n (Z.div d (Z.of_int 2))) d
-        else Z.div (Z.sub n (Z.div d (Z.of_int 2))) d in
-      to_real (Exact (Q.of_bigint near)) in
-    let approx_ops = fun v ->
+      let near =
+        if Z.geq n Z.zero then Z.div (Z.add n (Z.div d (Z.of_int 2))) d
+        else Z.div (Z.sub n (Z.div d (Z.of_int 2))) d
+      in
+      to_real (Exact (Q.of_bigint near))
+    in
+    let approx_ops =
+     fun v ->
       let to_real v = to_real (Approx v) in
       match op with
       | Neg -> to_real @@ Float.neg v
@@ -236,8 +239,10 @@ module Real = struct
       | Floor -> to_real @@ Float.floor v
       | Trunc -> to_real @@ Float.trunc v
       | Is_nan -> if Float.is_nan v then Value.True else Value.False
-      | _ -> eval_error (`Unsupported_operator (`Unop op, Ty_real)) in
-    let exact_ops = fun v ->
+      | _ -> eval_error (`Unsupported_operator (`Unop op, Ty_real))
+    in
+    let exact_ops =
+     fun v ->
       let to_real v = to_real (Exact v) in
       match op with
       | Neg -> to_real @@ Q.neg v
@@ -247,21 +252,21 @@ module Real = struct
       | Ceil -> to_real @@ Q.of_bigint @@ Z.cdiv (Q.num v) (Q.den v)
       | Floor -> to_real @@ Q.of_bigint @@ Z.fdiv (Q.num v) (Q.den v)
       | Trunc -> to_real @@ Q.of_bigint @@ Z.div (Q.num v) (Q.den v)
-      | Is_nan -> (match Q.classify v with
-        | Q.UNDEF -> Value.True
-        | _ -> Value.False)
-      | _ -> eval_error (`Unsupported_operator (`Unop op, Ty_real)) in
-    match v with
-      | Exact v -> exact_ops v
-      | Approx v -> approx_ops v
+      | Is_nan -> (
+        match Q.classify v with Q.UNDEF -> Value.True | _ -> Value.False )
+      | _ -> eval_error (`Unsupported_operator (`Unop op, Ty_real))
+    in
+    match v with Exact v -> exact_ops v | Approx v -> approx_ops v
 
   let binop (op : Ty.Binop.t) (v1 : Value.t) (v2 : Value.t) : Value.t =
     let rem_q (a : Q.t) (b : Q.t) : Q.t =
-      if Q.equal b Q.zero then eval_error (`Divide_by_zero);
+      if Q.equal b Q.zero then eval_error `Divide_by_zero;
       let div = Q.div a b in
       let k = Q.of_bigint (Z.div (Q.num div) (Q.den div)) in
-      Q.sub a (Q.mul b k) in
-    let approx_op v1 v2 : Value.real = match op with
+      Q.sub a (Q.mul b k)
+    in
+    let approx_op v1 v2 : Value.real =
+      match op with
       | Add -> Approx (Float.add v1 v2)
       | Sub -> Approx (Float.sub v1 v2)
       | Mul -> Approx (Float.mul v1 v2)
@@ -270,8 +275,10 @@ module Real = struct
       | Min -> Approx (Float.min v1 v2)
       | Max -> Approx (Float.max v1 v2)
       | Pow -> Approx (Float.pow v1 v2)
-      | _ -> eval_error (`Unsupported_operator (`Binop op, Ty_real)) in
-    let exact_op v1 v2 : Value.real = match op with
+      | _ -> eval_error (`Unsupported_operator (`Binop op, Ty_real))
+    in
+    let exact_op v1 v2 : Value.real =
+      match op with
       | Add -> Exact (Q.add v1 v2)
       | Sub -> Exact (Q.sub v1 v2)
       | Mul -> Exact (Q.mul v1 v2)
@@ -280,66 +287,76 @@ module Real = struct
       | Min -> Exact (Q.min v1 v2)
       | Max -> Exact (Q.max v1 v2)
       | Pow -> Approx (Float.pow (Q.to_float v1) (Q.to_float v2))
-      | _ -> eval_error (`Unsupported_operator (`Binop op, Ty_real)) in
+      | _ -> eval_error (`Unsupported_operator (`Binop op, Ty_real))
+    in
     let push_approx_op (v1 : Value.real) (v2 : Value.real) =
       match (v1, v2) with
       | Exact v1, Exact v2 -> exact_op v1 v2
       | Exact v1, Approx v2 -> approx_op (Q.to_float v1) v2
       | Approx v1, Exact v2 -> approx_op v1 (Q.to_float v2)
-      | Approx v1, Approx v2 -> approx_op v1 v2 in
-    to_real (push_approx_op (of_real 1 (`Binop op) v1) (of_real 2 (`Binop op) v2))
+      | Approx v1, Approx v2 -> approx_op v1 v2
+    in
+    to_real
+      (push_approx_op (of_real 1 (`Binop op) v1) (of_real 2 (`Binop op) v2))
 
   let relop (op : Ty.Relop.t) (v1 : Value.t) (v2 : Value.t) : bool =
-    let approx_op = match op with
+    let approx_op =
+      match op with
       | Lt -> Float.Infix.( < )
       | Le -> Float.Infix.( <= )
       | Gt -> Float.Infix.( > )
       | Ge -> Float.Infix.( >= )
       | Eq -> Float.Infix.( = )
       | Ne -> Float.Infix.( <> )
-      | _ -> eval_error (`Unsupported_operator (`Relop op, Ty_real)) in
-    let exact_op = match op with
+      | _ -> eval_error (`Unsupported_operator (`Relop op, Ty_real))
+    in
+    let exact_op =
+      match op with
       | Lt -> Q.lt
       | Le -> Q.leq
       | Gt -> Q.gt
       | Ge -> Q.geq
       | Eq -> Q.equal
       | Ne -> fun v1 v2 -> Fun.negate (Q.equal v1) v2
-      | _ -> eval_error (`Unsupported_operator (`Relop op, Ty_real)) in
+      | _ -> eval_error (`Unsupported_operator (`Relop op, Ty_real))
+    in
     let push_approx_op (v1 : Value.real) (v2 : Value.real) =
       match (v1, v2) with
       | Exact v1, Exact v2 -> exact_op v1 v2
       | Exact v1, Approx v2 -> approx_op (Q.to_float v1) v2
       | Approx v1, Exact v2 -> approx_op v1 (Q.to_float v2)
-      | Approx v1, Approx v2 -> approx_op v1 v2 in
+      | Approx v1, Approx v2 -> approx_op v1 v2
+    in
     push_approx_op (of_real 1 (`Relop op) v1) (of_real 2 (`Relop op) v2)
 
   let cvtop (op : Ty.Cvtop.t) (v : Value.t) : Value.t =
     let op' = `Cvtop op in
     match op with
-    | ToString -> Str begin
-      match (of_real 1 op' v) with
+    | ToString ->
+      Str
+        begin match of_real 1 op' v with
         | Exact v -> Q.to_string v
         | Approx v -> Float.to_string v
-    end
-    | OfString -> begin
-      match (of_str 1 op' v) with
-        | float_str when String.contains float_str '.' -> begin
-          match (Float.of_string_opt float_str) with
-            | Some f -> to_real (Approx f)
-            | None -> eval_error `Invalid_format_conversion
-        end
-        | q_str -> begin
-          try to_real (Exact (Q.of_string q_str))
-          with | _ -> eval_error `Invalid_format_conversion
         end
+    | OfString -> begin
+      match of_str 1 op' v with
+      | float_str when String.contains float_str '.' -> begin
+        match Float.of_string_opt float_str with
+        | Some f -> to_real (Approx f)
+        | None -> eval_error `Invalid_format_conversion
+      end
+      | q_str -> begin
+        try to_real (Exact (Q.of_string q_str))
+        with _ -> eval_error `Invalid_format_conversion
+      end
     end
     | Reinterpret_int -> to_real (Exact (Q.of_int @@ of_int 1 op' v))
-    | Reinterpret_float -> to_int begin
-      match (of_real 1 op' v) with
+    | Reinterpret_float ->
+      to_int
+        begin match of_real 1 op' v with
         | Exact v -> Q.to_int v
         | Approx v -> Float.to_int v
-    end
+        end
     | _ -> eval_error (`Unsupported_operator (op', Ty_real))
 end
 
diff --git a/src/smtml/expr.ml b/src/smtml/expr.ml
index e0669c2c..bbadc11c 100644
--- a/src/smtml/expr.ml
+++ b/src/smtml/expr.ml
@@ -398,14 +398,12 @@ let rec relop ty op hte1 hte2 =
     if Float.is_nan v || Float.is_infinite v then value True
     else raw_relop ty op hte1 hte2
   | Ty.Relop.Ne, Val (Real (Exact v)), _ | Ne, _, Val (Real (Exact v)) ->
-    if Fun.negate Q.is_real v then value True
-    else raw_relop ty op hte1 hte2
+    if Fun.negate Q.is_real v then value True else raw_relop ty op hte1 hte2
   | _, Val (Real (Approx v)), _ | _, _, Val (Real (Approx v)) ->
     if Float.is_nan v || Float.is_infinite v then value False
     else raw_relop ty op hte1 hte2
   | _, Val (Real (Exact v)), _ | _, _, Val (Real (Exact v)) ->
-    if Fun.negate Q.is_real v then value False
-    else raw_relop ty op hte1 hte2
+    if Fun.negate Q.is_real v then value False else raw_relop ty op hte1 hte2
   | Eq, _, Val Nothing | Eq, Val Nothing, _ -> value False
   | Ne, _, Val Nothing | Ne, Val Nothing, _ -> value True
   | Eq, _, Val (App (`Op "symbol", [ Str _ ]))
diff --git a/src/smtml/smtlib.ml b/src/smtml/smtlib.ml
index 71d1d036..14a9ad3d 100644
--- a/src/smtml/smtlib.ml
+++ b/src/smtml/smtlib.ml
@@ -108,7 +108,7 @@ module Term = struct
 
   let real ?loc (x : string) =
     try Expr.value (Real (Exact (Q.of_string x)))
-    with | _ -> Fmt.failwith "%ainvalid real" pp_loc loc
+    with _ -> Fmt.failwith "%ainvalid real" pp_loc loc
 
   let hexa ?loc:_ (h : string) =
     let len = String.length h in
diff --git a/src/smtml/value.ml b/src/smtml/value.ml
index 2a540f4a..05612f4b 100644
--- a/src/smtml/value.ml
+++ b/src/smtml/value.ml
@@ -4,7 +4,9 @@
 
 open Ty
 
-type real = Exact of Q.t | Approx of float
+type real =
+  | Exact of Q.t
+  | Approx of float
 
 type t =
   | True
@@ -126,7 +128,7 @@ let of_string (cast : Ty.t) v =
     | Some n -> Ok (Int n) )
   | Ty_real -> (
     try Ok (Real (Exact (Q.of_string v)))
-    with | _ -> Fmt.error_msg "invalid value %s, expected real" v)
+    with _ -> Fmt.error_msg "invalid value %s, expected real" v )
   | Ty_str -> Ok (Str v)
   | Ty_app | Ty_list | Ty_none | Ty_unit | Ty_regexp | Ty_roundingMode ->
     Fmt.error_msg "unsupported parsing values of type %a" Ty.pp cast
@@ -138,9 +140,9 @@ let rec to_json (v : t) : Yojson.Basic.t =
   | Unit -> `String "unit"
   | Int int -> `Int int
   | Real (Exact r) ->
-      let num = r |> Q.num |> Z.to_int in
-      let den = r |> Q.den |> Z.to_int in
-      `Assoc ["num", `Int num; "den", `Int den]
+    let num = r |> Q.num |> Z.to_int in
+    let den = r |> Q.den |> Z.to_int in
+    `Assoc [ ("num", `Int num); ("den", `Int den) ]
   | Real (Approx r) -> `Float r
   | Str str -> `String str
   | Num n -> Num.to_json n
diff --git a/src/smtml/value.mli b/src/smtml/value.mli
index 681d34ab..cd4f493c 100644
--- a/src/smtml/value.mli
+++ b/src/smtml/value.mli
@@ -9,8 +9,11 @@
 
 (** {1 Value Types} *)
 
-(** The type [real] represents either an exact rational, or an approximate float. *)
-type real = Exact of Q.t | Approx of float
+(** The type [real] represents either an exact rational, or an approximate
+    float. *)
+type real =
+  | Exact of Q.t
+  | Approx of float
 
 (** The type [t] represents concrete values. *)
 type t =
diff --git a/src/smtml/z3_mappings.default.ml b/src/smtml/z3_mappings.default.ml
index 198ca5f4..9737d1a4 100644
--- a/src/smtml/z3_mappings.default.ml
+++ b/src/smtml/z3_mappings.default.ml
@@ -41,9 +41,9 @@ module M = struct
     let int i = Z3.Arithmetic.Integer.mk_numeral_i ctx i
 
     let real (f : Value.real) =
-      let str = match f with
-        | Exact q -> Q.to_string q
-        | Approx f -> Float.to_string f in
+      let str =
+        match f with Exact q -> Q.to_string q | Approx f -> Float.to_string f
+      in
       Z3.Arithmetic.Real.mk_numeral_s ctx str
 
     let const sym ty = Z3.Expr.mk_const_s ctx sym ty
@@ -112,7 +112,8 @@ module M = struct
     module Interp = struct
       let to_int interp = Z.to_int @@ Z3.Arithmetic.Integer.get_big_int interp
 
-      let to_real interp : Value.real = Exact (Z3.Arithmetic.Real.get_ratio interp)
+      let to_real interp : Value.real =
+        Exact (Z3.Arithmetic.Real.get_ratio interp)
 
       let to_bool interp =
         match Z3.Boolean.get_bool_value interp with
diff --git a/test/unit/test_eval.ml b/test/unit/test_eval.ml
index f9b6664a..be85724e 100644
--- a/test/unit/test_eval.ml
+++ b/test/unit/test_eval.ml
@@ -172,7 +172,9 @@ module Real_test = struct
       assert_equal (real (Approx 7.)) result;
       let result = Eval.unop Ty_real Abs (real (Exact (Q.neg @@ Q.of_int 7))) in
       assert_equal (real (Exact (Q.of_int 7))) result;
-      let result = Eval.unop Ty_real Abs (real (Exact (Q.neg @@ Q.of_string "5/2"))) in
+      let result =
+        Eval.unop Ty_real Abs (real (Exact (Q.neg @@ Q.of_string "5/2")))
+      in
       assert_equal (real (Exact (Q.of_string "5/2"))) result
     in
     let test_sqrt _ =
@@ -184,29 +186,40 @@ module Real_test = struct
       assert_equal (real (Exact (Q.of_string "5/2"))) result
     in
     let test_nearest _ =
-      assert_equal (real (Approx 4.)) (Eval.unop Ty_real Nearest (real (Approx 4.2)));
-      assert_equal (real (Exact (Q.of_int 4))) (Eval.unop Ty_real Nearest (real (Exact (Q.of_string "42/10"))));
-      assert_equal (real (Approx 5.)) (Eval.unop Ty_real Nearest (real (Approx 4.6)));
-      assert_equal (real (Exact (Q.of_int 5))) (Eval.unop Ty_real Nearest (real (Exact (Q.of_string "46/10"))))
+      assert_equal (real (Approx 4.))
+        (Eval.unop Ty_real Nearest (real (Approx 4.2)));
+      assert_equal
+        (real (Exact (Q.of_int 4)))
+        (Eval.unop Ty_real Nearest (real (Exact (Q.of_string "42/10"))));
+      assert_equal (real (Approx 5.))
+        (Eval.unop Ty_real Nearest (real (Approx 4.6)));
+      assert_equal
+        (real (Exact (Q.of_int 5)))
+        (Eval.unop Ty_real Nearest (real (Exact (Q.of_string "46/10"))))
     in
     let test_ceil _ =
       let result = Eval.unop Ty_real Ceil (real (Approx 4.2)) in
       assert_equal (real (Approx 5.)) result;
-      let result = Eval.unop Ty_real Ceil (real (Exact (Q.of_string "42/10"))) in
+      let result =
+        Eval.unop Ty_real Ceil (real (Exact (Q.of_string "42/10")))
+      in
       assert_equal (real (Exact (Q.of_int 5))) result
     in
     let test_floor _ =
       let result = Eval.unop Ty_real Floor (real (Approx 4.2)) in
       assert_equal (real (Approx 4.)) result;
-      let result = Eval.unop Ty_real Floor (real (Exact (Q.of_string "42/10"))) in
+      let result =
+        Eval.unop Ty_real Floor (real (Exact (Q.of_string "42/10")))
+      in
       assert_equal (real (Exact (Q.of_int 4))) result
     in
     let test_trunc _ =
       let result = Eval.unop Ty_real Trunc (real (Approx Float.pi)) in
       assert_equal (real (Approx 3.)) result;
-      let result = Eval.unop Ty_real Trunc (real (Exact (Q.of_string "3.141592"))) in
+      let result =
+        Eval.unop Ty_real Trunc (real (Exact (Q.of_string "3.141592")))
+      in
       assert_equal (real (Exact (Q.of_int 3))) result
-
     in
     let test_is_nan _ =
       assert_equal (Eval.unop Ty_real Is_nan (real (Approx Float.nan))) true_;
@@ -231,65 +244,145 @@ module Real_test = struct
   (* Binary operators *)
   let binop =
     let test_add _ =
-      let result = Eval.binop Ty_real Add (real (Approx 2.)) (real (Approx 3.)) in
+      let result =
+        Eval.binop Ty_real Add (real (Approx 2.)) (real (Approx 3.))
+      in
       assert_equal (real (Approx 5.)) result;
-      let result = Eval.binop Ty_real Add (real (Exact (Q.of_int 2))) (real (Exact (Q.of_int 3))) in
+      let result =
+        Eval.binop Ty_real Add
+          (real (Exact (Q.of_int 2)))
+          (real (Exact (Q.of_int 3)))
+      in
       assert_equal (real (Exact (Q.of_int 5))) result;
-      let result = Eval.binop Ty_real Add (real (Exact (Q.of_string "2/3"))) (real (Exact (Q.of_string "1/3"))) in
-      assert_equal (real (Exact (Q.one))) result
+      let result =
+        Eval.binop Ty_real Add
+          (real (Exact (Q.of_string "2/3")))
+          (real (Exact (Q.of_string "1/3")))
+      in
+      assert_equal (real (Exact Q.one)) result
     in
     let test_sub _ =
-      let result = Eval.binop Ty_real Sub (real (Approx 3.)) (real (Approx 2.)) in
+      let result =
+        Eval.binop Ty_real Sub (real (Approx 3.)) (real (Approx 2.))
+      in
       assert_equal (real (Approx 1.)) result;
-      let result = Eval.binop Ty_real Sub (real (Exact (Q.of_int 3))) (real (Exact (Q.of_int 2))) in
+      let result =
+        Eval.binop Ty_real Sub
+          (real (Exact (Q.of_int 3)))
+          (real (Exact (Q.of_int 2)))
+      in
       assert_equal (real (Exact Q.one)) result;
-      let result = Eval.binop Ty_real Sub (real (Exact (Q.of_int 1))) (real (Exact (Q.of_string "1/3"))) in
+      let result =
+        Eval.binop Ty_real Sub
+          (real (Exact (Q.of_int 1)))
+          (real (Exact (Q.of_string "1/3")))
+      in
       assert_equal (real (Exact (Q.of_string "2/3"))) result
     in
     let test_mul _ =
-      let result = Eval.binop Ty_real Mul (real (Approx 3.)) (real (Approx 3.)) in
+      let result =
+        Eval.binop Ty_real Mul (real (Approx 3.)) (real (Approx 3.))
+      in
       assert_equal (real (Approx 9.)) result;
-      let result = Eval.binop Ty_real Mul (real (Exact (Q.of_int 3))) (real (Exact (Q.of_int 3))) in
+      let result =
+        Eval.binop Ty_real Mul
+          (real (Exact (Q.of_int 3)))
+          (real (Exact (Q.of_int 3)))
+      in
       assert_equal (real (Exact (Q.of_int 9))) result;
-      let result = Eval.binop Ty_real Mul (real (Exact (Q.of_string "2/3"))) (real (Exact (Q.of_int 2))) in
+      let result =
+        Eval.binop Ty_real Mul
+          (real (Exact (Q.of_string "2/3")))
+          (real (Exact (Q.of_int 2)))
+      in
       assert_equal (real (Exact (Q.of_string "4/3"))) result
     in
     let test_div _ =
-      let result = Eval.binop Ty_real Div (real (Approx 6.)) (real (Approx 3.)) in
+      let result =
+        Eval.binop Ty_real Div (real (Approx 6.)) (real (Approx 3.))
+      in
       assert_equal (real (Approx 2.)) result;
-      let result = Eval.binop Ty_real Div (real (Exact (Q.of_int 6))) (real (Exact (Q.of_int 3))) in
+      let result =
+        Eval.binop Ty_real Div
+          (real (Exact (Q.of_int 6)))
+          (real (Exact (Q.of_int 3)))
+      in
       assert_equal (real (Exact (Q.of_int 2))) result;
-      let result = Eval.binop Ty_real Div (real (Exact (Q.of_string "4/3"))) (real (Exact (Q.of_int 2))) in
+      let result =
+        Eval.binop Ty_real Div
+          (real (Exact (Q.of_string "4/3")))
+          (real (Exact (Q.of_int 2)))
+      in
       assert_equal (real (Exact (Q.of_string "2/3"))) result
     in
     let test_divide_by_zero _ =
-      let result = Eval.binop Ty_real Div (real (Approx 1.)) (real (Approx 0.)) in
+      let result =
+        Eval.binop Ty_real Div (real (Approx 1.)) (real (Approx 0.))
+      in
       assert_equal (real (Approx Float.infinity)) result;
-      let result = Eval.binop Ty_real Div (real (Exact Q.one)) (real (Exact Q.zero)) in
+      let result =
+        Eval.binop Ty_real Div (real (Exact Q.one)) (real (Exact Q.zero))
+      in
       assert_equal (real (Exact Q.inf)) result;
-      let result = Eval.binop Ty_real Div (real (Exact (Q.of_string "2/3"))) (real (Exact (Q.of_string "0/5"))) in
+      let result =
+        Eval.binop Ty_real Div
+          (real (Exact (Q.of_string "2/3")))
+          (real (Exact (Q.of_string "0/5")))
+      in
       assert_equal (real (Exact Q.inf)) result
     in
     let test_rem _ =
-      let result = Eval.binop Ty_real Rem (real (Approx 6.)) (real (Approx 3.)) in
+      let result =
+        Eval.binop Ty_real Rem (real (Approx 6.)) (real (Approx 3.))
+      in
       assert_equal (real (Approx 0.)) result;
-      let result = Eval.binop Ty_real Rem (real (Exact (Q.of_int 6))) (real (Exact (Q.of_int 3))) in
+      let result =
+        Eval.binop Ty_real Rem
+          (real (Exact (Q.of_int 6)))
+          (real (Exact (Q.of_int 3)))
+      in
       assert_equal (real (Exact Q.zero)) result;
-      let result = Eval.binop Ty_real Rem (real (Exact (Q.of_string "7/3"))) (real (Exact (Q.of_string "2/3"))) in
+      let result =
+        Eval.binop Ty_real Rem
+          (real (Exact (Q.of_string "7/3")))
+          (real (Exact (Q.of_string "2/3")))
+      in
       assert_equal (real (Exact (Q.of_string "1/3"))) result;
-      let result = Eval.binop Ty_real Rem (real (Exact (Q.of_string "-7/3"))) (real (Exact (Q.of_string "2/3"))) in
+      let result =
+        Eval.binop Ty_real Rem
+          (real (Exact (Q.of_string "-7/3")))
+          (real (Exact (Q.of_string "2/3")))
+      in
       assert_equal (real (Exact (Q.of_string "-1/3"))) result;
-      let result = Eval.binop Ty_real Rem (real (Exact (Q.of_string "5/2"))) (real (Exact (Q.of_string "1/2"))) in
+      let result =
+        Eval.binop Ty_real Rem
+          (real (Exact (Q.of_string "5/2")))
+          (real (Exact (Q.of_string "1/2")))
+      in
       assert_equal (real (Exact (Q.of_string "0/1"))) result;
-      let result = Eval.binop Ty_real Rem (real (Exact (Q.of_string "5/2"))) (real (Exact (Q.of_string "1/3"))) in
+      let result =
+        Eval.binop Ty_real Rem
+          (real (Exact (Q.of_string "5/2")))
+          (real (Exact (Q.of_string "1/3")))
+      in
       assert_equal (real (Exact (Q.of_string "1/6"))) result;
-      let result = Eval.binop Ty_real Rem (real (Exact (Q.of_string "-5/2"))) (real (Exact (Q.of_string "1/3"))) in
+      let result =
+        Eval.binop Ty_real Rem
+          (real (Exact (Q.of_string "-5/2")))
+          (real (Exact (Q.of_string "1/3")))
+      in
       assert_equal (real (Exact (Q.of_string "-1/6"))) result
     in
     let test_pow _ =
-      let result = Eval.binop Ty_real Pow (real (Approx 2.)) (real (Approx 3.)) in
+      let result =
+        Eval.binop Ty_real Pow (real (Approx 2.)) (real (Approx 3.))
+      in
       assert_equal (real (Approx 8.)) result;
-      let result = Eval.binop Ty_real Pow (real (Exact (Q.of_int 2))) (real (Exact (Q.of_int 3))) in
+      let result =
+        Eval.binop Ty_real Pow
+          (real (Exact (Q.of_int 2)))
+          (real (Exact (Q.of_int 3)))
+      in
       assert_equal (real (Approx 8.)) result
     in
     let test_min_max _ =
@@ -319,40 +412,77 @@ module Real_test = struct
   (* Relational operators *)
   let relop =
     let test_eq _ =
-      assert_bool "0.0 = 0.0" (Eval.relop Ty_real Eq (real (Approx 0.0)) (real (Approx 0.0)));
-      assert_bool "0 = 0" (Eval.relop Ty_real Eq (real (Exact Q.zero)) (real (Exact Q.zero)));
+      assert_bool "0.0 = 0.0"
+        (Eval.relop Ty_real Eq (real (Approx 0.0)) (real (Approx 0.0)));
+      assert_bool "0 = 0"
+        (Eval.relop Ty_real Eq (real (Exact Q.zero)) (real (Exact Q.zero)));
       assert_bool "nan != nan"
-        (not (Eval.relop Ty_real Eq (real (Approx Float.nan)) (real (Approx Float.nan))));
+        (not
+           (Eval.relop Ty_real Eq (real (Approx Float.nan))
+              (real (Approx Float.nan)) ) );
       assert_bool "undef != undef"
-        (not (Eval.relop Ty_real Eq (real (Exact Q.undef)) (real (Exact Q.undef))))
+        (not
+           (Eval.relop Ty_real Eq (real (Exact Q.undef)) (real (Exact Q.undef))) )
     in
     let test_ne _ =
-      assert_bool "0.0 = 0.0" (not (Eval.relop Ty_real Ne (real (Approx 0.0)) (real (Approx 0.0))));
-      assert_bool "0 = 0" (not (Eval.relop Ty_real Ne (real (Exact Q.zero)) (real (Exact Q.zero))));
+      assert_bool "0.0 = 0.0"
+        (not (Eval.relop Ty_real Ne (real (Approx 0.0)) (real (Approx 0.0))));
+      assert_bool "0 = 0"
+        (not
+           (Eval.relop Ty_real Ne (real (Exact Q.zero)) (real (Exact Q.zero))) );
       assert_bool "nan != nan"
-        (Eval.relop Ty_real Ne (real (Approx Float.nan)) (real (Approx Float.nan)));
+        (Eval.relop Ty_real Ne (real (Approx Float.nan))
+           (real (Approx Float.nan)) );
       assert_bool "undef != undef"
         (Eval.relop Ty_real Ne (real (Exact Q.undef)) (real (Exact Q.undef)))
     in
     let test_lt _ =
-      assert_bool "2.0 < 3.0" (Eval.relop Ty_real Lt (real (Approx 2.)) (real (Approx 3.)));
-      assert_bool "2 < 3" (Eval.relop Ty_real Lt (real (Exact (Q.of_int 2))) (real (Exact (Q.of_int 3))));
-      assert_bool "2/3 < 3/3" (Eval.relop Ty_real Lt (real (Exact (Q.of_string "2/3"))) (real (Exact (Q.of_string "3/3"))))
+      assert_bool "2.0 < 3.0"
+        (Eval.relop Ty_real Lt (real (Approx 2.)) (real (Approx 3.)));
+      assert_bool "2 < 3"
+        (Eval.relop Ty_real Lt
+           (real (Exact (Q.of_int 2)))
+           (real (Exact (Q.of_int 3))) );
+      assert_bool "2/3 < 3/3"
+        (Eval.relop Ty_real Lt
+           (real (Exact (Q.of_string "2/3")))
+           (real (Exact (Q.of_string "3/3"))) )
     in
     let test_le _ =
-      assert_bool "2.0 <= 3.0" (Eval.relop Ty_real Le (real (Approx 2.)) (real (Approx 3.)));
-      assert_bool "2 <= 3" (Eval.relop Ty_real Le (real (Exact (Q.of_int 2))) (real (Exact (Q.of_int 3))));
-      assert_bool "2/3 <= 3/3" (Eval.relop Ty_real Le (real (Exact (Q.of_string "2/3"))) (real (Exact (Q.of_string "3/3"))))
+      assert_bool "2.0 <= 3.0"
+        (Eval.relop Ty_real Le (real (Approx 2.)) (real (Approx 3.)));
+      assert_bool "2 <= 3"
+        (Eval.relop Ty_real Le
+           (real (Exact (Q.of_int 2)))
+           (real (Exact (Q.of_int 3))) );
+      assert_bool "2/3 <= 3/3"
+        (Eval.relop Ty_real Le
+           (real (Exact (Q.of_string "2/3")))
+           (real (Exact (Q.of_string "3/3"))) )
     in
     let test_gt _ =
-      assert_bool "4.0 > 3.0" (Eval.relop Ty_real Gt (real (Approx 4.)) (real (Approx 3.)));
-      assert_bool "4 > 3" (Eval.relop Ty_real Gt (real (Exact (Q.of_int 4))) (real (Exact (Q.of_int 3))));
-      assert_bool "1/3 > 1/4" (Eval.relop Ty_real Gt (real (Exact (Q.of_string "1/3"))) (real (Exact (Q.of_string "1/4"))))
+      assert_bool "4.0 > 3.0"
+        (Eval.relop Ty_real Gt (real (Approx 4.)) (real (Approx 3.)));
+      assert_bool "4 > 3"
+        (Eval.relop Ty_real Gt
+           (real (Exact (Q.of_int 4)))
+           (real (Exact (Q.of_int 3))) );
+      assert_bool "1/3 > 1/4"
+        (Eval.relop Ty_real Gt
+           (real (Exact (Q.of_string "1/3")))
+           (real (Exact (Q.of_string "1/4"))) )
     in
     let test_ge _ =
-      assert_bool "4.0 >= 3.0" (Eval.relop Ty_real Ge (real (Approx 4.)) (real (Approx 3.)));
-      assert_bool "4 >= 3" (Eval.relop Ty_real Ge (real (Exact (Q.of_int 4))) (real (Exact (Q.of_int 3))));
-      assert_bool "1/3 >= 1/4" (Eval.relop Ty_real Ge (real (Exact (Q.of_string "1/3"))) (real (Exact (Q.of_string "1/4"))))
+      assert_bool "4.0 >= 3.0"
+        (Eval.relop Ty_real Ge (real (Approx 4.)) (real (Approx 3.)));
+      assert_bool "4 >= 3"
+        (Eval.relop Ty_real Ge
+           (real (Exact (Q.of_int 4)))
+           (real (Exact (Q.of_int 3))) );
+      assert_bool "1/3 >= 1/4"
+        (Eval.relop Ty_real Ge
+           (real (Exact (Q.of_string "1/3")))
+           (real (Exact (Q.of_string "1/4"))) )
     in
 
     [ "test_eq" >:: test_eq
diff --git a/test/unit/test_expr.ml b/test/unit/test_expr.ml
index 45706587..6f382a15 100644
--- a/test/unit/test_expr.ml
+++ b/test/unit/test_expr.ml
@@ -173,15 +173,26 @@ let test_binop_real_exact _ =
   let real r = real (Exact r) in
   let open Q in
   check (Expr.binop ty Add (real zero) (real (of_int 42))) (real (of_int 42));
-  check (Expr.binop ty Add (real (of_string "2/3")) (real (of_string "1/3"))) (real one);
+  check
+    (Expr.binop ty Add (real (of_string "2/3")) (real (of_string "1/3")))
+    (real one);
   check (Expr.binop ty Sub (real zero) (real one)) (real (neg one));
-  check (Expr.binop ty Mul (real (of_int 2)) (real (of_int 21))) (real (of_int 42));
-  check (Expr.binop ty Mul (real (of_string "1/3")) (real (of_int 2))) (real (of_string "2/3"));
-  check (Expr.binop ty Div (real (of_int 84)) (real (of_int 2))) (real (of_int 42));
+  check
+    (Expr.binop ty Mul (real (of_int 2)) (real (of_int 21)))
+    (real (of_int 42));
+  check
+    (Expr.binop ty Mul (real (of_string "1/3")) (real (of_int 2)))
+    (real (of_string "2/3"));
+  check
+    (Expr.binop ty Div (real (of_int 84)) (real (of_int 2)))
+    (real (of_int 42));
   check (Expr.binop ty Rem (real zero) (real one)) (real zero);
-  check (Expr.binop ty Min (real (of_int 2)) (real (of_int 4))) (real (of_int 2));
-  check (Expr.binop ty Max (real (of_int 2)) (real (of_int 4))) (real (of_int 4))
-
+  check
+    (Expr.binop ty Min (real (of_int 2)) (real (of_int 4)))
+    (real (of_int 2));
+  check
+    (Expr.binop ty Max (real (of_int 2)) (real (of_int 4)))
+    (real (of_int 4))
 
 let test_binop_string _ =
   let open Infix in