diff --git a/src_colibri2/tests/solve/smt_fp/sat/dune.inc b/src_colibri2/tests/solve/smt_fp/sat/dune.inc
index 06de62e82806f22c01bdc768fc98c9d5b4fdb372..ec4f35a9963de46541e38050fbd3c1641774895d 100644
--- a/src_colibri2/tests/solve/smt_fp/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_fp/sat/dune.inc
@@ -13,6 +13,10 @@
 (rule (alias runtest) (action (diff oracle recognize_float64.smt2.res)))
 (rule (action (with-stdout-to recognize_rounding_mode.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:recognize_rounding_mode.smt2}))))
 (rule (alias runtest) (action (diff oracle recognize_rounding_mode.smt2.res)))
+(rule (action (with-stdout-to rm_instanciation.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:rm_instanciation.smt2}))))
+(rule (alias runtest) (action (diff oracle rm_instanciation.smt2.res)))
+(rule (action (with-stdout-to rm_universal.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:rm_universal.smt2}))))
+(rule (alias runtest) (action (diff oracle rm_universal.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}))))
diff --git a/src_colibri2/tests/solve/smt_fp/sat/rm_instanciation.smt2 b/src_colibri2/tests/solve/smt_fp/sat/rm_instanciation.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..f881999439bff2f9f5f5ca1f62afe46b6336c187
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/rm_instanciation.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+(declare-fun x () (_ FloatingPoint 8 24))
+(declare-fun y () (_ FloatingPoint 8 24))
+(declare-fun m () RoundingMode)
+(assert (not (= RNE m)))
+(assert (= (fp.add m x y) x))
+(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/tests/solve/smt_fp/sat/rm_universal.smt2 b/src_colibri2/tests/solve/smt_fp/sat/rm_universal.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..78a5beceda606d4b277bf2f590023a237712ce33
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/sat/rm_universal.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(declare-fun x () (_ FloatingPoint 8 24))
+(declare-fun y () (_ FloatingPoint 8 24))
+(assert (forall ((m RoundingMode)) (= (fp.add m x y) x)))
+(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/tests/solve/smt_fp/unsat/dune b/src_colibri2/tests/solve/smt_fp/unsat/dune
new file mode 100644
index 0000000000000000000000000000000000000000..6d9fe5883f08bc15b92dc715d3c58c193023dbb5
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/unsat/dune
@@ -0,0 +1,13 @@
+(include dune.inc)
+
+(rule
+ (alias runtest)
+ (deps
+  (glob_files *.cnf)
+  (glob_files *.smt2)
+  (glob_files *.psmt2))
+ (action
+  (with-stdout-to
+   dune.inc
+   (run %{exe:../../../generate_tests/generate_dune_tests.exe} . unsat)))
+ (mode promote))
diff --git a/src_colibri2/tests/solve/smt_fp/unsat/dune.inc b/src_colibri2/tests/solve/smt_fp/unsat/dune.inc
new file mode 100644
index 0000000000000000000000000000000000000000..21f8594898e2a66c3ca7196688f1f338ce729e60
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/unsat/dune.inc
@@ -0,0 +1,3 @@
+(rule (action (with-stdout-to oracle (echo "unsat\n"))))
+(rule (action (with-stdout-to inf_pos_neg_neq.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:inf_pos_neg_neq.smt2}))))
+(rule (alias runtest) (action (diff oracle inf_pos_neg_neq.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_fp/unsat/f32_f64_incompatible.smt2 b/src_colibri2/tests/solve/smt_fp/unsat/f32_f64_incompatible.smt2
deleted file mode 100644
index fdc81481ad8535a4a8787e20ec17c8619f95328a..0000000000000000000000000000000000000000
--- a/src_colibri2/tests/solve/smt_fp/unsat/f32_f64_incompatible.smt2
+++ /dev/null
@@ -1,5 +0,0 @@
-(set-logic ALL)
-(declare-fun x () (_ FloatingPoint 11 53))
-(declare-fun y () (_ FloatingPoint 8 24))
-(assert (= x y))
-(check-sat)
\ No newline at end of file
diff --git a/src_colibri2/tests/solve/smt_fp/unsat/inf_pos_neg_neq.smt2 b/src_colibri2/tests/solve/smt_fp/unsat/inf_pos_neg_neq.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..3e7669912bd18cd3f61847c639ba4a4174f88c9d
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_fp/unsat/inf_pos_neg_neq.smt2
@@ -0,0 +1,3 @@
+(set-logic ALL)
+(assert (fp.eq (_ +oo 8 24) (_ -oo 8 24)))
+(check-sat)
\ No newline at end of file