diff --git a/colibri2/tests/solve/all/both/ceil1.smt2 b/colibri2/tests/solve/all/both/ceil1.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..ca23f5937b2cb3d3a147b6042b7a75c8d1a1e283
--- /dev/null
+++ b/colibri2/tests/solve/all/both/ceil1.smt2
@@ -0,0 +1,13 @@
+(set-logic ALL)
+
+(declare-fun x1 () Real)
+(declare-fun x2 () Real)
+
+(assert (= x1 (colibri_ceil x2)))
+
+(assert (<= 2.5 x2 3.5))
+
+(assert (! (<= 3 x1 4) :colibri2 goal))
+
+
+(check-sat)
diff --git a/colibri2/tests/solve/all/both/ceil2.smt2 b/colibri2/tests/solve/all/both/ceil2.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..8e173e5b5c2034b7202e22e2bb2767a551d1717a
--- /dev/null
+++ b/colibri2/tests/solve/all/both/ceil2.smt2
@@ -0,0 +1,13 @@
+(set-logic ALL)
+
+(declare-fun x1 () Real)
+(declare-fun x2 () Real)
+
+(assert (= x1 (colibri_ceil x2)))
+
+(assert (<= (- 3.5) x2 (- 2.5)))
+
+(assert (! (<= (- 3) x1 (- 2)) :colibri2 goal))
+
+
+(check-sat)
diff --git a/colibri2/tests/solve/all/both/dune b/colibri2/tests/solve/all/both/dune
new file mode 100644
index 0000000000000000000000000000000000000000..b1c6bc252e79bcccd3fa5cef5dc6acd29b1e48ad
--- /dev/null
+++ b/colibri2/tests/solve/all/both/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} . both)))
+ (mode promote))
diff --git a/colibri2/tests/solve/all/both/dune.inc b/colibri2/tests/solve/all/both/dune.inc
new file mode 100644
index 0000000000000000000000000000000000000000..0a6481640e7d1dadbf313118eed52d71edb1c4f0
--- /dev/null
+++ b/colibri2/tests/solve/all/both/dune.inc
@@ -0,0 +1,18 @@
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --negate-goal 
+--dont-print-result %{dep:ceil1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --negate-goal --learning --dont-print-result %{dep:ceil1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat 
+--dont-print-result %{dep:ceil1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:ceil1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --negate-goal 
+--dont-print-result %{dep:ceil2.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --negate-goal --learning --dont-print-result %{dep:ceil2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat 
+--dont-print-result %{dep:ceil2.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:ceil2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --negate-goal 
+--dont-print-result %{dep:floor1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --negate-goal --learning --dont-print-result %{dep:floor1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat 
+--dont-print-result %{dep:floor1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:floor1.smt2})) (package colibri2))
diff --git a/colibri2/tests/solve/all/both/floor1.smt2 b/colibri2/tests/solve/all/both/floor1.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..e6c3904ae338131c216e7976d3389cba2c585e49
--- /dev/null
+++ b/colibri2/tests/solve/all/both/floor1.smt2
@@ -0,0 +1,13 @@
+(set-logic ALL)
+
+(declare-fun x1 () Real)
+(declare-fun x2 () Real)
+
+(assert (= x1 (colibri_floor x2)))
+
+(assert (<= 2.5 x2 3.5))
+
+(assert (! (<= 2 x1 3) :colibri2 goal))
+
+
+(check-sat)
diff --git a/colibri2/tests/solve/all/unsat/dune.inc b/colibri2/tests/solve/all/unsat/dune.inc
index c84d1e6c69c7da71aedaf78081961e9597199d2f..584dd91c3a5ecc40c21effb59ca08fc3dc8d6835 100644
--- a/colibri2/tests/solve/all/unsat/dune.inc
+++ b/colibri2/tests/solve/all/unsat/dune.inc
@@ -55,3 +55,6 @@
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:work_with_fourier_not_simplex2.psmt2})) (package colibri2))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:work_with_fourier_not_simplex2.psmt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
+--dont-print-result %{dep:wp_initialize.psmt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:wp_initialize.psmt2})) (package colibri2))
diff --git a/colibri2/tests/solve/smt_nra/both/dune b/colibri2/tests/solve/smt_nra/both/dune
new file mode 100644
index 0000000000000000000000000000000000000000..0807a2205366a5e1e1d667738bdea82750f48243
--- /dev/null
+++ b/colibri2/tests/solve/smt_nra/both/dune
@@ -0,0 +1,12 @@
+(include dune.inc)
+
+(rule
+ (alias runtest)
+ (deps
+  (glob_files *.cnf)
+  (glob_files *.smt2))
+ (action
+  (with-stdout-to
+   dune.inc
+   (run %{exe:../../../generate_tests/generate_dune_tests.exe} . both)))
+ (mode promote))
diff --git a/colibri2/tests/solve/smt_nra/both/dune.inc b/colibri2/tests/solve/smt_nra/both/dune.inc
new file mode 100644
index 0000000000000000000000000000000000000000..bfd9904d282c15b4da698f14c4aaeaee4b0c0a3c
--- /dev/null
+++ b/colibri2/tests/solve/smt_nra/both/dune.inc
@@ -0,0 +1,6 @@
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --negate-goal 
+--dont-print-result %{dep:propa1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --negate-goal --learning --dont-print-result %{dep:propa1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat 
+--dont-print-result %{dep:propa1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:propa1.smt2})) (package colibri2))
diff --git a/colibri2/tests/solve/smt_nra/both/propa1.smt2 b/colibri2/tests/solve/smt_nra/both/propa1.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..c9b3bc02cff4e96733f27ae2bbfd9a8bbf8dae47
--- /dev/null
+++ b/colibri2/tests/solve/smt_nra/both/propa1.smt2
@@ -0,0 +1,40 @@
+(set-logic ALL)
+
+(declare-fun x () Real)
+(declare-fun y () Real)
+
+(assert (< 1 x 10))
+(assert (and (< 1 y) (<= y 10)))
+
+(define-fun f ((a Real)(b Real)) Real (+ (/ (/ (- (* x y) y) (+ y 1)) 12.0) 1))
+
+(define-fun z1_1 () Real (f x y))
+(define-fun z2_1 () Real (f y x))
+
+(define-fun z1_2 () Real (f z1_1 z2_1))
+(define-fun z2_2 () Real (f z2_1 z1_1))
+
+(define-fun z1_3 () Real (f z1_2 z2_2))
+(define-fun z2_3 () Real (f z2_2 z1_2))
+
+(define-fun z1_4 () Real (f z1_3 z2_3))
+(define-fun z2_4 () Real (f z2_3 z1_3))
+
+(define-fun z1_5 () Real (f z1_4 z2_4))
+(define-fun z2_5 () Real (f z2_4 z1_4))
+
+(define-fun z1_6 () Real (f z1_5 z2_5))
+(define-fun z2_6 () Real (f z2_5 z1_5))
+
+(define-fun z1_7 () Real (f z1_6 z2_6))
+(define-fun z2_7 () Real (f z2_6 z1_6))
+
+(define-fun z1_8 () Real (f z1_7 z2_7))
+(define-fun z2_8 () Real (f z2_7 z1_8))
+
+(define-fun z1_9 () Real (f z1_8 z2_8))
+(define-fun z2_9 () Real (f z2_8 z1_8))
+
+
+(assert (! (and (< 0.0 z1_9 10.0) (< 0.0 z2_9 10.0))  :colibri2 goal))
+(check-sat)