diff --git a/src_colibri2/tests/solve/smt_fp/sat/dune.inc b/src_colibri2/tests/solve/smt_fp/sat/dune.inc
index 317cd2282153480fd6e02f5cce20d0243a5db96e..7c0354f447f06bed19458c07fc9b72e24395f360 100644
--- a/src_colibri2/tests/solve/smt_fp/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_fp/sat/dune.inc
@@ -7,5 +7,7 @@
 (rule (alias runtest) (action (diff oracle recognize_rounding_mode.smt2.res)))
 (rule (action (with-stdout-to simple_add_float32.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:simple_add_float32.smt2}))))
 (rule (alias runtest) (action (diff oracle simple_add_float32.smt2.res)))
+(rule (action (with-stdout-to simple_eq_float32.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:simple_eq_float32.smt2}))))
+(rule (alias runtest) (action (diff oracle simple_eq_float32.smt2.res)))
 (rule (action (with-stdout-to simple_mul_float32.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:simple_mul_float32.smt2}))))
 (rule (alias runtest) (action (diff oracle simple_mul_float32.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_fp/sat/simple_eq_float32.smt2 b/src_colibri2/tests/solve/smt_fp/sat/simple_eq_float32.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..11abb9fe5b5a84f4ad0720a9e282a4cc74c5efd7
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/simple_eq_float32.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(declare-fun x () (_ FloatingPoint 8 24))
+(declare-fun y () (_ FloatingPoint 8 24))
+(assert (fp.eq (fp.add RNE x y) x))
+(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/theories/FP/float32.ml b/src_colibri2/theories/FP/float32.ml
index 7a641d43ef25665c9d4f556aa29a1415c67e3207..7e8bf13190712466f91d9e9ba8be4a50fa97f39a 100644
--- a/src_colibri2/theories/FP/float32.ml
+++ b/src_colibri2/theories/FP/float32.ml
@@ -47,6 +47,7 @@ let compute_ground d t =
   let (!>>) t = Rounding_mode.value (Rounding_mode.coerce_nodevalue (interp d t )) in
   let (!>) t = Float32.value (Float32.coerce_nodevalue (interp d t)) in
   let (!<) v = `Some (Float32.nodevalue (Float32.index v)) in
+  let (!<<) v = `Some (Boolean.BoolValue.nodevalue (Boolean.BoolValue.index v)) in
   match Ground.sem t with
   | { app = {builtin = Expr.Fp_add (8, 24); _}; args; _} ->
     let m, a, b = IArray.extract3_exn args in
@@ -64,6 +65,21 @@ let compute_ground d t =
     let m, a, b = IArray.extract3_exn args in
     if Farith.B32.(eq !>b (zero true) || eq !>b (zero false)) then `Uninterp
     else !< (Farith.B32.div !>>m !>a !>b)
+  | { app = {builtin = Expr.Fp_eq (8, 24); _}; args; _} ->
+    let a, b = IArray.extract2_exn args in
+    !<< (Farith.B32.eq !>a !>b)
+  | { app = {builtin = Expr.Fp_leq (8, 24); _}; args; _} ->
+    let a, b = IArray.extract2_exn args in
+    !<< (Farith.B32.le !>a !>b)
+  | { app = {builtin = Expr.Fp_lt (8, 24); _}; args; _} ->
+    let a, b = IArray.extract2_exn args in
+    !<< (Farith.B32.lt !>a !>b)
+  | { app = {builtin = Expr.Fp_geq (8, 24); _}; args; _} ->
+    let a, b = IArray.extract2_exn args in
+    !<< (Farith.B32.ge !>a !>b)
+  | { app = {builtin = Expr.Fp_gt (8, 24); _}; args; _} ->
+    let a, b = IArray.extract2_exn args in
+    !<< (Farith.B32.gt !>a !>b)
   | _ -> `None
 
 let init_check d = Interp.Register.check d (fun d t ->
@@ -155,6 +171,13 @@ let converter d (f:Ground.t) =
     List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;b]
   in
   match Ground.sem f with
+  | {app={builtin=Expr.Fp_abs (8, 24); _}; args; _} ->
+    let a = IArray.extract1_exn args in
+    reg a; attach d f;
+    let wait =
+      set r (let+ va = get a in Farith.B32.abs va)
+    in
+    List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a; r]
   | {app={builtin=Expr.Fp_add (8, 24); _}; args; _} ->
     let m, a, b = IArray.extract3_exn args in
     reg m; reg a; reg b; attach d f;
diff --git a/src_colibri2/theories/FP/fp_value.mli b/src_colibri2/theories/FP/fp_value.mli
index 947ebe72488c432b5bc40e75fb601fba4c378c1e..62ee723d8eb59adb0e1ed5e12834c51418fd062d 100644
--- a/src_colibri2/theories/FP/fp_value.mli
+++ b/src_colibri2/theories/FP/fp_value.mli
@@ -26,7 +26,7 @@ val posint_sequence : Z.t Base.Sequence.t
 (** Names (string) wrapped in a module *)
 module type FloatName = sig val name : string end
 
-(** 
+(**
    Helper to extend a module of type [Farith.S] into a module of
    type [ValueKind.Value]
 *)