diff --git a/src_colibri2/tests/solve/smt_fp/sat/simple_add_float32.smt2 b/src_colibri2/tests/solve/smt_fp/sat/simple_add_float32.smt2
index 6dc5136f73f62b889896dac0db2c57af53b12a53..6f0a55c4ef55157052764d0a2b7c12ed868ede9b 100644
--- a/src_colibri2/tests/solve/smt_fp/sat/simple_add_float32.smt2
+++ b/src_colibri2/tests/solve/smt_fp/sat/simple_add_float32.smt2
@@ -1,5 +1,5 @@
 (set-logic ALL)
 (declare-fun x () (_ FloatingPoint 8 24))
 (declare-fun y () (_ FloatingPoint 8 24))
-(assert (= (fp.add RNE x y) (fp.add RNE x y)))
+(assert (= (fp.add RNE x y) x))
 (check-sat)
\ No newline at end of file
diff --git a/src_colibri2/tests/solve/smt_fp/sat/simple_mul_float32.smt2 b/src_colibri2/tests/solve/smt_fp/sat/simple_mul_float32.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..e0e38f6736112c5a4924579cd4cfa9b4897845de
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/simple_mul_float32.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(declare-fun x () (_ FloatingPoint 8 24))
+(declare-fun y () (_ FloatingPoint 8 24))
+(assert (= (fp.mul 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 c05d22bae2b2d8ae99d5a4ff7b779dc27e8c4176..063738b310a92f81be9515224a5f77f9a1a45fcf 100644
--- a/src_colibri2/theories/FP/float32.ml
+++ b/src_colibri2/theories/FP/float32.ml
@@ -43,25 +43,26 @@ let init_ty d =
 let interp d n = Opt.get_exn Impossible (Egraph.get_value d n)
 
 let compute_ground d t =
-
-  (* let mode = function
-     | Expr.RoundNearestTiesToEven -> Farith.NE
-     | Expr.RoundNearestTiesToAway -> Farith.NA
-     | Expr.RoundTowardPositive    -> Farith.UP
-     | Expr.RoundTowardNegative    -> Farith.DN
-     | Expr.RoundTowardZero        -> Farith.ZR
-     | _                           -> raise Impossible
-     in *)
-
   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
-
   match Ground.sem t with
   | { app = {builtin = Expr.Fp_add (8, 24); _}; args; _} ->
-    (* TODO: get the mode *)
     let m, a, b = IArray.extract3_exn args in
     !< (Farith.B32.add !>>m !>a !>b)
+  | { app = {builtin = Expr.Fp_sub (8, 24); _}; args; _} ->
+    let m, a, b = IArray.extract3_exn args in
+    !< (Farith.B32.sub !>>m !>a !>b)
+  | { app = {builtin = Expr.Fp_mul (8, 24); _}; args; _} ->
+    let m, a, b = IArray.extract3_exn args in
+    !< (Farith.B32.mul !>>m !>a !>b)
+  | { app = {builtin = Expr.Fp_abs (8, 24); _}; args; _} ->
+    let a = IArray.extract1_exn args in
+    !< (Farith.B32.abs !>a)
+  | { app = {builtin = Expr.Fp_div (8, 24); _}; args; _} ->
+    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)
   | _ -> `None
 
 let init_check d = Interp.Register.check d (fun d t ->
@@ -71,6 +72,9 @@ let init_check d = Interp.Register.check d (fun d t ->
     match compute_ground d t with
     | `None -> None
     | `Some v -> Some (check v)
+    | `Uninterp ->
+      (* TODO : Give the control to the Uniterpreted Symbols theory *)
+      None
   )
 
 let init env =
diff --git a/src_colibri2/theories/FP/fp.ml b/src_colibri2/theories/FP/fp.ml
index ce8138c8f88746aa05be897109db9ad40df0b126..bfe29e98840fbee81c176539b975b1a4beb8cf84 100644
--- a/src_colibri2/theories/FP/fp.ml
+++ b/src_colibri2/theories/FP/fp.ml
@@ -25,6 +25,12 @@ let converter d f =
   match Ground.sem f with
   | { app = {builtin = Expr.Fp_add (_, _); _}; args; _ } ->
     IArray.iter ~f:reg args
+  | { app = {builtin = Expr.Fp_sub (_, _); _}; args; _ } ->
+    IArray.iter ~f:reg args
+  | { app = {builtin = Expr.Fp_div (_, _); _}; args; _ } ->
+    IArray.iter ~f:reg args
+  | { app = {builtin = Expr.Fp_mul (_, _); _}; args; _ } ->
+    IArray.iter ~f:reg args
   | _ -> ()
 
 let th_register env =
diff --git a/src_colibri2/theories/FP/fp_value.ml b/src_colibri2/theories/FP/fp_value.ml
index 471f575c1e885d776865e025b573f0660f689a8f..067a95eb12bb04465b07c2f5867cd28eb56e3459 100644
--- a/src_colibri2/theories/FP/fp_value.ml
+++ b/src_colibri2/theories/FP/fp_value.ml
@@ -53,4 +53,3 @@ let posint_sequence_without_zero =
 (** Generate the sequence of positive integers (without 0) *)
 let posint_sequence =
   Base.Sequence.shift_right posint_sequence_without_zero Z.zero
-
diff --git a/src_colibri2/theories/FP/rounding_mode.ml b/src_colibri2/theories/FP/rounding_mode.ml
index a45335f4e6d07d0879cf82c747518092cc87fad7..ecb6699353a41379113d429a75c31a41646ab454 100644
--- a/src_colibri2/theories/FP/rounding_mode.ml
+++ b/src_colibri2/theories/FP/rounding_mode.ml
@@ -82,7 +82,7 @@ let init_ty d =
 
 let interp d n = Opt.get_exn Impossible (Egraph.get_value d n)
 
-let compute_ground _ t =
+let compute_cst t =
   let (!<) v = `Some (Modes.nodevalue (Modes.index v)) in
   match Ground.sem t with
   | { app = {builtin = Expr.RoundNearestTiesToEven; _}; _} ->
@@ -101,7 +101,7 @@ let init_check d = Interp.Register.check d (fun d t ->
     let check r =
       Value.equal r (interp d (Ground.node t))
     in
-    match compute_ground d t with
+    match compute_cst t with
     | `None -> None
     | `Some v -> Some (check v)
   )