diff --git a/src_colibri2/tests/generate_tests/generate_dune_tests.ml b/src_colibri2/tests/generate_tests/generate_dune_tests.ml
index 2df700bb6e2661f8ccd3eccef6bec9bbd796cb88..7a3261dd8dce452d2df53cfff8f78152a7e9101c 100644
--- a/src_colibri2/tests/generate_tests/generate_dune_tests.ml
+++ b/src_colibri2/tests/generate_tests/generate_dune_tests.ml
@@ -22,7 +22,7 @@ let dir = Sys.argv.(1)
 
 let result = if Array.length Sys.argv >= 3 then Some Sys.argv.(2) else None
 
-let cmd = "%{bin:colibri2} --size=15M --time=30s --max-steps 3500"
+let cmd = "%{bin:colibri2} --size=20M --time=30s --max-steps 3500"
 
 let print_test cout file =
   match result with
diff --git a/src_colibri2/tests/solve/all/sat/dune.inc b/src_colibri2/tests/solve/all/sat/dune.inc
index 4e0cd3e0bba21ec1769c54205e80729a14233335..c126645af6fe337a080b2d8a6df208797cf706da 100644
--- a/src_colibri2/tests/solve/all/sat/dune.inc
+++ b/src_colibri2/tests/solve/all/sat/dune.inc
@@ -1,9 +1,9 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:div_abs.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:div_abs.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:div_abs.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:div_abs2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:div_abs2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:div_abs2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:union-Union-is_singletonqtvc_2.psmt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:union-Union-is_singletonqtvc_2.psmt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:union-Union-is_singletonqtvc_2.psmt2})))
diff --git a/src_colibri2/tests/solve/all/steplimitreached/dune.inc b/src_colibri2/tests/solve/all/steplimitreached/dune.inc
index 98b899ea73a26e035e0584d4b0ce4aaedad0905e..fd122a1a6da60943efcc010ee7b11f07df1e3b37 100644
--- a/src_colibri2/tests/solve/all/steplimitreached/dune.inc
+++ b/src_colibri2/tests/solve/all/steplimitreached/dune.inc
@@ -1,3 +1,3 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status steplimitreached 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status steplimitreached 
 --dont-print-result %{dep:bag-BagImpl-addqtvc.psmt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status steplimitreached --learning --dont-print-result %{dep:bag-BagImpl-addqtvc.psmt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status steplimitreached --learning --dont-print-result %{dep:bag-BagImpl-addqtvc.psmt2})))
diff --git a/src_colibri2/tests/solve/all/unsat/dune.inc b/src_colibri2/tests/solve/all/unsat/dune.inc
index 857492e6d430d352e4e82554a51515d413431615..6ecfee75469ac55e3028628eefe5ffd6a90e76e0 100644
--- a/src_colibri2/tests/solve/all/unsat/dune.inc
+++ b/src_colibri2/tests/solve/all/unsat/dune.inc
@@ -1,24 +1,24 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:bag-BagImpl-createqtvc.psmt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:bag-BagImpl-createqtvc.psmt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:bag-BagImpl-createqtvc.psmt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:div_abs.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:div_abs.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:div_abs.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:fact-FactRecursive-fact_recqtvc.psmt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:fact-FactRecursive-fact_recqtvc.psmt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:fact-FactRecursive-fact_recqtvc.psmt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:interval-Convexe-exists_memqtvc_1.psmt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:interval-Convexe-exists_memqtvc_1.psmt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:interval-Convexe-exists_memqtvc_1.psmt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:interval-Convexe-exists_memqtvc_2.psmt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:interval-Convexe-exists_memqtvc_2.psmt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:interval-Convexe-exists_memqtvc_2.psmt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:mul_abs.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_abs.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_abs.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:union-Union-is_singletonqtvc_1.psmt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:union-Union-is_singletonqtvc_1.psmt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:union-Union-is_singletonqtvc_1.psmt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:union-Union-length0_positiveqtvc_1.psmt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:union-Union-length0_positiveqtvc_1.psmt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:union-Union-length0_positiveqtvc_1.psmt2})))
diff --git a/src_colibri2/tests/solve/dimacs/sat/dune.inc b/src_colibri2/tests/solve/dimacs/sat/dune.inc
index 3a8a918a67df7e466836bcb7c234e24ee7fcdd91..5d40389aae1868d08563657cd4a2f3ce181d8f82 100644
--- a/src_colibri2/tests/solve/dimacs/sat/dune.inc
+++ b/src_colibri2/tests/solve/dimacs/sat/dune.inc
@@ -1,33 +1,33 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:anomaly_agetooold.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:anomaly_agetooold.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:anomaly_agetooold.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:anomaly_agetooold2.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:anomaly_agetooold2.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:anomaly_agetooold2.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:assertion_fail.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:assertion_fail.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:assertion_fail.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:fuzzing1.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:fuzzing1.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:fuzzing1.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:fuzzing2.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:fuzzing2.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:fuzzing2.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:par8-1-c.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:par8-1-c.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:par8-1-c.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:pigeon-2.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:pigeon-2.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:pigeon-2.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:pigeon-3.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:pigeon-3.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:pigeon-3.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:pigeon-4.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:pigeon-4.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:pigeon-4.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:quinn.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:quinn.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:quinn.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:simple_v3_c2.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:simple_v3_c2.cnf})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:simple_v3_c2.cnf})))
diff --git a/src_colibri2/tests/solve/dimacs/unsat/dune.inc b/src_colibri2/tests/solve/dimacs/unsat/dune.inc
index a4da599a19b005f9759869cda3cddbc91e8a27fd..148c9a4ec88ff5c3b32f1ec773361a1d8ac10387 100644
--- a/src_colibri2/tests/solve/dimacs/unsat/dune.inc
+++ b/src_colibri2/tests/solve/dimacs/unsat/dune.inc
@@ -1,18 +1,18 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:anomaly_agetooold.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:anomaly_agetooold.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:anomaly_agetooold.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:modus_ponens.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:modus_ponens.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:modus_ponens.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:pigeon-1.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:pigeon-1.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:pigeon-1.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:pigeon-2.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:pigeon-2.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:pigeon-2.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:pigeon-3.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:pigeon-3.cnf})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:pigeon-3.cnf})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:pigeon-4.cnf})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:pigeon-4.cnf})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:pigeon-4.cnf})))
diff --git a/src_colibri2/tests/solve/models/dune.inc b/src_colibri2/tests/solve/models/dune.inc
index c9eaba0f3712b7401bd9cbf990aa709bdf7bc93d..7b35329d06e34b17f8a94b92ffd2c693cfc8b257 100644
--- a/src_colibri2/tests/solve/models/dune.inc
+++ b/src_colibri2/tests/solve/models/dune.inc
@@ -1,4 +1,4 @@
-(rule (action (with-stdout-to abs_real.smt2.res (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status colibri2 %{dep:abs_real.smt2}))))
+(rule (action (with-stdout-to abs_real.smt2.res (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status colibri2 %{dep:abs_real.smt2}))))
 (rule (alias runtest) (action (diff abs_real.smt2.oracle abs_real.smt2.res)))
-(rule (action (with-stdout-to get_value.smt2.res (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status colibri2 %{dep:get_value.smt2}))))
+(rule (action (with-stdout-to get_value.smt2.res (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status colibri2 %{dep:get_value.smt2}))))
 (rule (alias runtest) (action (diff get_value.smt2.oracle get_value.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_adt/sat/dune.inc b/src_colibri2/tests/solve/smt_adt/sat/dune.inc
index 8e7e09be40b1350daabfd7868cad647e76b43834..53f078718eca53ccc0c9ade8489e9a665c18b045 100644
--- a/src_colibri2/tests/solve/smt_adt/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_adt/sat/dune.inc
@@ -1,18 +1,18 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:enum.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:enum.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:enum.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:list0.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:list0.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:list0.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:list1.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:list1.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:list1.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:tree1.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:tree1.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:tree1.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:tree2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:tree2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:tree2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:tree3.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:tree3.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:tree3.smt2})))
diff --git a/src_colibri2/tests/solve/smt_adt/unsat/dune.inc b/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
index 76424e820adb599eb4103225c0826c56eaddfbc3..f3f9ebb8725e8c2edf0ae69002dfc2fad92c9a4d 100644
--- a/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
@@ -1,24 +1,24 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:enum.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:enum.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:enum.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:enum2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:enum2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:enum2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:list0.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:list0.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:list0.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:list1.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:list1.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:list1.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:list2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:list2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:list2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:list3.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:list3.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:list3.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:list4.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:list4.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:list4.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:parlist0.psmt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:parlist0.psmt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:parlist0.psmt2})))
diff --git a/src_colibri2/tests/solve/smt_fp/dune.inc b/src_colibri2/tests/solve/smt_fp/dune.inc
index 3df67fbfaa78aeed8624cc20b8b429a4cdd6f680..755fd7c18d1b59ad560a40cdd9ed2ab31af67723 100644
--- a/src_colibri2/tests/solve/smt_fp/dune.inc
+++ b/src_colibri2/tests/solve/smt_fp/dune.inc
@@ -1,2 +1,2 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result %{dep:rm_universal.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result --learning %{dep:rm_universal.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result %{dep:rm_universal.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result --learning %{dep:rm_universal.smt2})))
diff --git a/src_colibri2/tests/solve/smt_fp/sat/dune.inc b/src_colibri2/tests/solve/smt_fp/sat/dune.inc
index a37aae0c7467a9349b619a24789a534a76c4ae72..cea27603ac70b52060d77c77333f6de8fe1d2ce2 100644
--- a/src_colibri2/tests/solve/smt_fp/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_fp/sat/dune.inc
@@ -1,45 +1,45 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:exists_eq_not_fp_eq.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:exists_eq_not_fp_eq.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:exists_eq_not_fp_eq.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:inf_pos_neg_neq_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:inf_pos_neg_neq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:inf_pos_neg_neq_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:infm_eq_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:infm_eq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:infm_eq_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:infp_eq_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:infp_eq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:infp_eq_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:nan_neq_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:nan_neq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:nan_neq_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:recognize_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:recognize_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:recognize_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:recognize_rounding_mode.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:recognize_rounding_mode.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:recognize_rounding_mode.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:rm_instanciation.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:rm_instanciation.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:rm_instanciation.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:simple_add_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:simple_add_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:simple_add_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:simple_eq_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:simple_eq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:simple_eq_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:simple_mul_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:simple_mul_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:simple_mul_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:to_fp_eq_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:to_fp_eq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:to_fp_eq_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:zero_pos_neg_neq_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:zero_pos_neg_neq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:zero_pos_neg_neq_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:zerom_eq_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:zerom_eq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:zerom_eq_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:zerop_eq_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:zerop_eq_float32.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:zerop_eq_float32.smt2})))
diff --git a/src_colibri2/tests/solve/smt_fp/unsat/dune.inc b/src_colibri2/tests/solve/smt_fp/unsat/dune.inc
index df78d2aeadad850713c9ff0c4205176e2eba52aa..7e79bd0e4d2abc2828c55f16bf061474f3a71c43 100644
--- a/src_colibri2/tests/solve/smt_fp/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_fp/unsat/dune.inc
@@ -1,12 +1,12 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:eq_fp_eq.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:eq_fp_eq.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:eq_fp_eq.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:inf_pos_neg_neq.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:inf_pos_neg_neq.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:inf_pos_neg_neq.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:nan_neq_float32.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:nan_neq_float32.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:nan_neq_float32.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:propagate_le_ge.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:propagate_le_ge.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:propagate_le_ge.smt2})))
diff --git a/src_colibri2/tests/solve/smt_lra/sat/dune.inc b/src_colibri2/tests/solve/smt_lra/sat/dune.inc
index c2743209c79e5a0af1b4f715e7ddb0361c8f8466..b7855698a5e71c020b300128ea800062e79f7f99 100644
--- a/src_colibri2/tests/solve/smt_lra/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_lra/sat/dune.inc
@@ -1,102 +1,102 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_CombiRepr_normalize.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_CombiRepr_normalize.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_CombiRepr_normalize.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_conflict_add_disequality.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_conflict_add_disequality.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_conflict_add_disequality.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_conpoly.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_conpoly.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_conpoly.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_decide_must_test_is_dis_equal.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_decide_must_test_is_dis_equal.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_decide_must_test_is_dis_equal.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_init_always_merge_itself.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_init_always_merge_itself.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_init_always_merge_itself.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_init_and_propa_must_be_ordered.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_init_and_propa_must_be_ordered.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_init_and_propa_must_be_ordered.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_merge_case1.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_case1.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_case1.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_merge_case_4.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_case_4.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_case_4.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_merge_case_4_bis.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_case_4_bis.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_case_4_bis.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_merge_itself_coef_of_repr_is_one.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_itself_coef_of_repr_is_one.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_itself_coef_of_repr_is_one.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_merge_itself_last_case.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_itself_last_case.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_itself_last_case.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_merge_itself_pivot_not_in_p12.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_itself_pivot_not_in_p12.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_itself_pivot_not_in_p12.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_merge_must_use_find.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_must_use_find.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_merge_must_use_find.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_mult_explication.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_mult_explication.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_mult_explication.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_mult_not_linear_in_conflict.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_mult_not_linear_in_conflict.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_mult_not_linear_in_conflict.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_normalize_use_find_def.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_normalize_use_find_def.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_normalize_use_find_def.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_own_repr.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_own_repr.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_own_repr.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_propacl.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_propacl.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_propacl.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_subst_and_conflict_add.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_subst_and_conflict_add.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_subst_and_conflict_add.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:arith_zero_dom.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_zero_dom.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:arith_zero_dom.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:attach_only_when_dom_present.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:attach_only_when_dom_present.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:attach_only_when_dom_present.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:init_not_repr.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:init_not_repr.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:init_not_repr.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:le.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:le.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:le.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:le2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:le2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:le2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:mul.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:mul.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:mul.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:sem_invariant_in_learnt_dec.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:sem_invariant_in_learnt_dec.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:sem_invariant_in_learnt_dec.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:solver_add_pexp_cl.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:solver_add_pexp_cl.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:solver_add_pexp_cl.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:solver_arith_homogeneous_dist_sign.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:solver_arith_homogeneous_dist_sign.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:solver_arith_homogeneous_dist_sign.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:solver_merge_itself_repr_inside.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:solver_merge_itself_repr_inside.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:solver_merge_itself_repr_inside.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:solver_set_pending_merge_expsameexp.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:solver_set_pending_merge_expsameexp.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:solver_set_pending_merge_expsameexp.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:solver_subst_eventdom_find.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:solver_subst_eventdom_find.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:solver_subst_eventdom_find.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:to_real.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:to_real.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:to_real.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:to_real2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:to_real2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:to_real2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:zero_should_not_be_simplified.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:zero_should_not_be_simplified.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:zero_should_not_be_simplified.smt2})))
diff --git a/src_colibri2/tests/solve/smt_lra/unsat/dune.inc b/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
index 148c56f234b5deb1bad0a638588d467da421fd0f..35fe81049402a61edd9e131d0ecd5e8abadfb549 100644
--- a/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_lra/unsat/dune.inc
@@ -1,33 +1,33 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:arith_ExpMult_by_zero.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:arith_ExpMult_by_zero.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:arith_ExpMult_by_zero.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:arith_merge_case2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:arith_merge_case2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:arith_merge_case2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:le.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:le.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:le.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:le2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:le2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:le2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:mul.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:repr_and_poly.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:repr_and_poly.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:repr_and_poly.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:repr_fourier.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:repr_fourier.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:repr_fourier.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:solver_merge_itself_repr_empty.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:solver_merge_itself_repr_empty.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:solver_merge_itself_repr_empty.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:solver_set_sem_merge_sign.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:solver_set_sem_merge_sign.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:solver_set_sem_merge_sign.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:to_real.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:to_real.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:to_real.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:to_real2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:to_real2.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:to_real2.smt2})))
diff --git a/src_colibri2/tests/solve/smt_nra/sat/dune.inc b/src_colibri2/tests/solve/smt_nra/sat/dune.inc
index c73a28514ac43c5079afe957dbae5b47804a2ca1..c2bb7f7b087bbcd64ea93469ee8989a82e93324b 100644
--- a/src_colibri2/tests/solve/smt_nra/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_nra/sat/dune.inc
@@ -1,21 +1,21 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:ceil.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:ceil.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:ceil.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:div_pos.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:div_pos.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:div_pos.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:div_pos_lt.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:div_pos_lt.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:div_pos_lt.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:mul_commut.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:mul_commut.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:mul_commut.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:mul_commut2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:mul_commut2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:mul_commut2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:mul_pos.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:mul_pos.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:mul_pos.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:mul_pos_lt.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:mul_pos_lt.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:mul_pos_lt.smt2})))
diff --git a/src_colibri2/tests/solve/smt_nra/unsat/dune.inc b/src_colibri2/tests/solve/smt_nra/unsat/dune.inc
index e25ae6b8c2aa2a031c4271477e527e4d1a5499d4..02cd7cc165673b25a7a3506d2acf5520d9a59b3a 100644
--- a/src_colibri2/tests/solve/smt_nra/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_nra/unsat/dune.inc
@@ -1,30 +1,30 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:ceil.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:ceil.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:ceil.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:div_pos.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:div_pos.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:div_pos.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:div_pos_lt.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:div_pos_lt.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:div_pos_lt.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:div_pos_lt_to_real.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:div_pos_lt_to_real.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:div_pos_lt_to_real.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:floor.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:floor.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:floor.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:mul_commut.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_commut.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_commut.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:mul_commut2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_commut2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_commut2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:mul_pos.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_pos.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_pos.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:mul_pos_lt.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_pos_lt.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_pos_lt.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:mul_pos_zero_le.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_pos_zero_le.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_pos_zero_le.smt2})))
diff --git a/src_colibri2/tests/solve/smt_quant/dune.inc b/src_colibri2/tests/solve/smt_quant/dune.inc
index 7ff5d8dec7552006dcfca2c9198ccdf8fa613f12..6d35d86dc60cd0c0419c3e722b69bcfb9842336c 100644
--- a/src_colibri2/tests/solve/smt_quant/dune.inc
+++ b/src_colibri2/tests/solve/smt_quant/dune.inc
@@ -1,6 +1,8 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result %{dep:forall0.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result --learning %{dep:forall0.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result %{dep:forall3.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result --learning %{dep:forall3.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result %{dep:forall4.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result --learning %{dep:forall4.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result %{dep:forall0.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result --learning %{dep:forall0.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result %{dep:forall3.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result --learning %{dep:forall3.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result %{dep:forall4.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result --learning %{dep:forall4.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result %{dep:multitrigger.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status colibri2 --dont-print-result --learning %{dep:multitrigger.smt2})))
diff --git a/src_colibri2/tests/solve/smt_quant/multitrigger.smt2 b/src_colibri2/tests/solve/smt_quant/multitrigger.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..65cd62885781b3311efd3289b5add031969a500a
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_quant/multitrigger.smt2
@@ -0,0 +1,13 @@
+(set-logic ALL)
+(set-info :status-colibri2 unsat)
+
+(declare-sort S 0)
+(declare-fun P (S) Bool)
+
+(assert (forall ((x S)(y S)) (=> (P x) (P y))))
+
+(declare-fun a () S)
+(declare-fun b () S)
+(assert (P a))
+(assert (not (P b)))
+(check-sat)
diff --git a/src_colibri2/tests/solve/smt_quant/sat/dune.inc b/src_colibri2/tests/solve/smt_quant/sat/dune.inc
index d33efa7a088a3f513006663b225c230b89037e1d..82ec2986da343c3b2354fdf4f9980161812d461b 100644
--- a/src_colibri2/tests/solve/smt_quant/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_quant/sat/dune.inc
@@ -1,3 +1,3 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:exists.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:exists.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:exists.smt2})))
diff --git a/src_colibri2/tests/solve/smt_quant/unsat/dune.inc b/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
index 517624de8395acfd45a3e1d50c99aa837e6ae91b..3ca854bdf577fd786339cf4c24edd0ec0c1ee40f 100644
--- a/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
@@ -1,33 +1,33 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:exists.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:exists.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:exists.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:exists2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:exists2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:exists2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:forall0.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall0.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall0.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:forall1.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall1.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall1.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:forall2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:forall3.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall3.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall3.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:forall4.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall4.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall4.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:forall5.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall5.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall5.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:forall6.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall6.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall6.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:forall7.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall7.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall7.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:forall8.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall8.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:forall8.smt2})))
diff --git a/src_colibri2/tests/solve/smt_uf/sat/dune.inc b/src_colibri2/tests/solve/smt_uf/sat/dune.inc
index 1ab95cb3d0d149b7b713ddcd730c5553dd02d7d1..e39fff7d19c008c68e39859cf93914c86f524624 100644
--- a/src_colibri2/tests/solve/smt_uf/sat/dune.inc
+++ b/src_colibri2/tests/solve/smt_uf/sat/dune.inc
@@ -1,63 +1,63 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:bad_conflict.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:bad_conflict.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:bad_conflict.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:bcp_dont_like_duplicate.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:bcp_dont_like_duplicate.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:bcp_dont_like_duplicate.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:bool_not_propa.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:bool_not_propa.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:bool_not_propa.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:boolexpup.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:boolexpup.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:boolexpup.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:clause_normalization.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:clause_normalization.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:clause_normalization.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:clmerge.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:clmerge.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:clmerge.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:conflict_complete_needed_cl.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:conflict_complete_needed_cl.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:conflict_complete_needed_cl.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:directdom_not.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:directdom_not.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:directdom_not.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:dis_dom_before_first_age.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:dis_dom_before_first_age.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:dis_dom_before_first_age.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:dom_merge_equality.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:dom_merge_equality.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:dom_merge_equality.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:equality.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:equality.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:equality.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:equality_condis.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:equality_condis.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:equality_condis.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:equality_get_sem.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:equality_get_sem.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:equality_get_sem.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:exp_sem_equality.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:exp_sem_equality.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:exp_sem_equality.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:explimit_cl_equality.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:explimit_cl_equality.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:explimit_cl_equality.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:implication.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:implication.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:implication.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:intmap_set_disjoint.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:intmap_set_disjoint.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:intmap_set_disjoint.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:is_equal_not_propagated.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:is_equal_not_propagated.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:is_equal_not_propagated.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:ite_sem_bool.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:ite_sem_bool.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:ite_sem_bool.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:polyeq_genequality.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:polyeq_genequality.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:polyeq_genequality.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:substupfalse_equality.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:substupfalse_equality.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:substupfalse_equality.smt2})))
diff --git a/src_colibri2/tests/solve/smt_uf/unsat/dune.inc b/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
index e29ac13dd0c6f2ef96e2ee757bc02792782d5fd6..941a3d34d0c5e8e910af801db33e7f04871a36f8 100644
--- a/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
@@ -1,39 +1,39 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:NEQ004_size4__decide_eq_us.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:NEQ004_size4__decide_eq_us.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:NEQ004_size4__decide_eq_us.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:deltaed0.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:deltaed0.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:deltaed0.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:diff_to_value_for_bool.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:diff_to_value_for_bool.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:diff_to_value_for_bool.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:diff_value_substupfalse.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:diff_value_substupfalse.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:diff_value_substupfalse.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:distinct.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:distinct.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:distinct.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:eq_diamond2.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:eq_diamond2.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:eq_diamond2.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:equality_norm_set.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:equality_norm_set.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:equality_norm_set.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:fundef.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:fundef.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:fundef.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:get_repr_at__instead_of__equal_CRepr.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:get_repr_at__instead_of__equal_CRepr.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:get_repr_at__instead_of__equal_CRepr.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:many_distinct.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:many_distinct.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:many_distinct.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:polyeq_genequality.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:polyeq_genequality.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:polyeq_genequality.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:polyeq_genequality_deltaed.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:polyeq_genequality_deltaed.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:polyeq_genequality_deltaed.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:xor.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=15M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:xor.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:xor.smt2})))
diff --git a/src_colibri2/theories/quantifier/InvertedPath.ml b/src_colibri2/theories/quantifier/InvertedPath.ml
index 124dc033cd89fa1be480dddb4ccab4b4f005f833..ed3ea87c763b8537b00c38a674182d3195925d29 100644
--- a/src_colibri2/theories/quantifier/InvertedPath.ml
+++ b/src_colibri2/theories/quantifier/InvertedPath.ml
@@ -29,8 +29,11 @@ open Common
   *)
 
 type t' = {
+  triggers : Trigger.t list;  (** triggers reached *)
   matches : t Pattern.M.t;
-  triggers : Trigger.t list;
+      (** Pattern to match the node against next top down *)
+  any_matches : t Pattern.M.t;
+      (** Pattern to match the any node against next top down *)
   ups :
     (Expr.Ty.t list
     * Pattern.t IArray.t
@@ -38,13 +41,20 @@ type t' = {
     * t)
     list
     F_Pos.M.t;
+      (** pattern to match the node against next bottom up *)
 }
+(** All the alternative path to continue in parallel *)
 
 and t = t' Context.Ref.t [@@deriving show]
 
 let create creator =
   Context.Ref.create creator
-    { matches = Pattern.M.empty; triggers = []; ups = F_Pos.M.empty }
+    {
+      matches = Pattern.M.empty;
+      any_matches = Pattern.M.empty;
+      triggers = [];
+      ups = F_Pos.M.empty;
+    }
 
 let rec exec d acc substs n ip =
   Debug.dprintf5 debug_full "[Quant] Exec: %a, %a[%i]" Node.pp n
@@ -68,6 +78,14 @@ let rec exec d acc substs n ip =
           exec d acc substs n ip)
         acc ip.matches
     in
+    let acc =
+      Pattern.M.fold_left
+        (fun acc p ip ->
+          Debug.dprintf2 debug_full "[Quant] Exec match %a" Pattern.pp p;
+          let substs = Pattern.match_any_term d substs p in
+          exec d acc substs n ip)
+        acc ip.any_matches
+    in
     let acc =
       let match_one_app (ptyl, pargs, pos, t) acc g =
         let { Ground.tyargs = tyl; args; _ } = Ground.sem g in
@@ -117,7 +135,7 @@ let pt_ips =
 (** parent-node, wait for a subterm with the right class *)
 let pn_ips = HPN.create Fmt.nop "Quantifier.pn" (fun c _ -> create c)
 
-let add_pattern pat ip =
+let add_trigger pat ip =
   Context.Ref.set ip
   @@
   let ip = Context.Ref.get ip in
@@ -133,6 +151,16 @@ let add_match pat ipr =
       @@ { ip with matches = Pattern.M.add pat ip' ip.matches };
       ip'
 
+let add_any_match pat ipr =
+  let ip = Context.Ref.get ipr in
+  match Pattern.M.find_opt pat ip.any_matches with
+  | Some ip' -> ip'
+  | None ->
+      let ip' = create (Context.Ref.creator ipr) in
+      Context.Ref.set ipr
+      @@ { ip with any_matches = Pattern.M.add pat ip' ip.any_matches };
+      ip'
+
 let add_up f_pos tytl tl ipr =
   let ip = Context.Ref.get ipr in
   let ip' = create (Context.Ref.creator ipr) in
@@ -153,7 +181,8 @@ let insert_pattern d (trigger : Trigger.t) =
         let pairs =
           List.filter
             (fun pp ->
-              (* possible just parent1 only one path is needed by pairs *)
+              (* improvement: possible to limit to just parent1 since only one
+                 path is needed by pairs *)
               F_Pos.equal fp pp.PP.parent1 || F_Pos.equal fp pp.PP.parent2)
             pairs
         in
@@ -182,9 +211,15 @@ let insert_pattern d (trigger : Trigger.t) =
         ips @ acc)
       ~init:[] tl
   in
-  let pp_vars = Pattern.get_pps trigger.pat in
+  let pp_vars = Pattern.get_pps trigger.pat [] in
   match trigger.pat with
   | Var _ | Node _ -> ()
   | App (f, tytl, tl) ->
       let ips = insert_children pp_vars f tytl tl in
-      List.iter (add_pattern trigger) ips
+      let ips =
+        List.map
+          (fun ip ->
+            List.fold_left (fun ip p -> add_any_match p ip) ip trigger.pats)
+          ips
+      in
+      List.iter (add_trigger trigger) ips
diff --git a/src_colibri2/theories/quantifier/pattern.ml b/src_colibri2/theories/quantifier/pattern.ml
index ebe4baf212d410b7871f3e63b384c1730dd54bfd..cc61f03e0dc2106529b969110e8b27eb1b25c500 100644
--- a/src_colibri2/theories/quantifier/pattern.ml
+++ b/src_colibri2/theories/quantifier/pattern.ml
@@ -115,9 +115,9 @@ let rec match_ty substs (ty : Ground.Ty.t) (p : Expr.Ty.t) : Ground.Subst.S.t =
 
 let rec match_term d (substs : Ground.Subst.S.t) (n : Node.t) (p : t) :
     Ground.Subst.S.t =
-  Debug.dprintf4 debug_full "[Quant] matching %a %a" pp p Node.pp n;
   if Ground.Subst.S.is_empty substs then substs
-  else
+  else (
+    Debug.dprintf4 debug_full "[Quant] matching %a %a" pp p Node.pp n;
     match p with
     | Var v ->
         let match_ty (acc : Ground.Subst.S.t) ty : Ground.Subst.S.t =
@@ -159,7 +159,7 @@ let rec match_term d (substs : Ground.Subst.S.t) (n : Node.t) (p : t) :
               in
               Ground.Subst.S.union substs acc)
           Ground.Subst.S.empty s
-    | Node n' -> if Egraph.is_equal d n n' then substs else Ground.Subst.S.empty
+    | Node n' -> if Egraph.is_equal d n n' then substs else Ground.Subst.S.empty)
 
 let rec check_ty subst (ty : Ground.Ty.t) (p : Expr.Ty.t) : bool =
   match p.ty_descr with
@@ -257,7 +257,7 @@ let rec check_term_exists_exn d (subst : Ground.Subst.t) (p : t) : Node.S.t =
 let check_term_exists d (subst : Ground.Subst.t) (p : t) : Node.S.t =
   try check_term_exists_exn d subst p with Not_found -> Node.S.empty
 
-let get_pps pattern =
+let get_pps pattern patterns =
   let rec aux acc fp p =
     match p with
     | Var v ->
@@ -268,22 +268,31 @@ let get_pps pattern =
           ~init:acc tl
     | Node _ -> acc
   in
-  let m =
-    match pattern with
-    | Var _ | Node _ -> Expr.Term.Var.M.empty
-    | App (f, _, tl) ->
-        IArray.foldi
-          ~f:(fun pos acc p -> aux acc F_Pos.{ f; pos } p)
-          ~init:Expr.Term.Var.M.empty tl
+  let compute_position =
+    List.fold_left
+      (fun acc pattern ->
+        match pattern with
+        | Var _ | Node _ -> acc
+        | App (f, _, tl) ->
+            IArray.foldi
+              ~f:(fun pos acc p -> aux acc F_Pos.{ f; pos } p)
+              ~init:acc tl)
+      Expr.Term.Var.M.empty
   in
-  Expr.Term.Var.M.map
-    (fun s ->
+  let m = compute_position [ pattern ] in
+  let ms = compute_position patterns in
+  Expr.Term.Var.M.mapi
+    (fun v s ->
       let l = F_Pos.S.elements s in
+      let ls =
+        Expr.Term.Var.M.find_def F_Pos.S.empty v ms
+        |> F_Pos.S.union s |> F_Pos.S.elements
+      in
       Lists.fold_product
         (fun acc parents1 parents2 ->
           if F_Pos.equal parents1 parents2 then acc
           else PP.create parents1 parents2 :: acc)
-        [] l l)
+        [] l ls)
     m
 
 let env_ground_by_apps =
diff --git a/src_colibri2/theories/quantifier/pattern.mli b/src_colibri2/theories/quantifier/pattern.mli
index a71c4405a0b8a5746e8a310245dd24d4443f813f..252a806f9bd6150397d496145feb871fd3520fb1 100644
--- a/src_colibri2/theories/quantifier/pattern.mli
+++ b/src_colibri2/theories/quantifier/pattern.mli
@@ -50,7 +50,7 @@ val check_ty : Ground.Subst.t -> Ground.Ty.t -> Expr.Ty.t -> bool
     is equal to ty *)
 
 val check_term : _ Egraph.t -> Ground.Subst.t -> Node.t -> t -> bool
-(** [check_term d subst n pat] checks the pattern [pat] subsituted by [subst] is
+(** [check_term d subst n pat] checks the pattern [pat] substituted by [subst] is
    equal by congruence of [d] to [n] *)
 
 val check_term_exists : _ Egraph.t -> Ground.Subst.t -> t -> Node.S.t
@@ -62,8 +62,9 @@ val match_any_term : _ Egraph.t -> Ground.Subst.S.t -> t -> Ground.Subst.S.t
    for each substitution. Each return substitution corresponds to one given as
    input. *)
 
-val get_pps : t -> PP.t list Expr.Term.Var.M.t
-(** [get_pps pat] return the parent-parent pairs in [pat] for each variables *)
+val get_pps : t -> t list -> PP.t list Expr.Term.Var.M.t
+(** [get_pps pat pats] return for each variables the parent-parent pairs between
+   position in [pat] and position in [pat] or [pats] *)
 
 val env_ground_by_apps : Ground.t Context.Push.t F.EnvApps.t
 (** The set of ground terms sorted by their top function *)
diff --git a/src_colibri2/theories/quantifier/quantifier.ml b/src_colibri2/theories/quantifier/quantifier.ml
index f6f9a061fa797a1232920ddcd2ad242ac036dff2..c1dff258d955d2a8da91b6a67bd3e14e8d2ad809 100644
--- a/src_colibri2/theories/quantifier/quantifier.ml
+++ b/src_colibri2/theories/quantifier/quantifier.ml
@@ -27,7 +27,11 @@ open Common
 let add_trigger d t =
   Trigger.add_trigger d t;
   InvertedPath.insert_pattern d t;
-  let substs = Pattern.match_any_term d Pattern.init t.pat in
+  let substs =
+    List.fold_left
+      (fun acc pat -> Pattern.match_any_term d acc pat)
+      Pattern.init (t.pat :: t.pats)
+  in
   Ground.Subst.S.iter (Trigger.instantiate d t) substs
 
 let find_new_event d n (info : Info.t) n' (info' : Info.t) =
@@ -221,7 +225,11 @@ let attach d th =
           in
           Debug.dprintf4 debug "[Quant] For %a adds %a"
             Ground.ClosedQuantifier.pp th
-            Fmt.(list ~sep:semi (Fmt.using (fun t -> t.Trigger.pat) Pattern.pp))
+            Fmt.(
+              list ~sep:semi
+                (Fmt.using
+                   (fun t -> t.Trigger.pats)
+                   (list ~sep:comma Pattern.pp)))
             triggers;
           List.iter (add_trigger d) triggers
       (* Todo match with current terms *))
diff --git a/src_colibri2/theories/quantifier/trigger.ml b/src_colibri2/theories/quantifier/trigger.ml
index d36a61b665743f0d9ca689b985038be536d8cbdf..255166ef538be16722fe78478402f9e1edb64540 100644
--- a/src_colibri2/theories/quantifier/trigger.ml
+++ b/src_colibri2/theories/quantifier/trigger.ml
@@ -26,6 +26,7 @@ module T = struct
 
   type t = {
     pat : Pattern.t;
+    pats : Pattern.t list;
     checks : Pattern.t list;
     form : Ground.ClosedQuantifier.t;
     eager : bool;
@@ -33,7 +34,9 @@ module T = struct
   [@@deriving eq, ord, hash]
 
   let pp fmt t =
-    Fmt.pf fmt "[%a, %a -> %a]" Pattern.pp t.pat
+    Fmt.pf fmt "[%a, %a ( %a ) -> %a]" Pattern.pp t.pat
+      Fmt.(list ~sep:comma Pattern.pp)
+      t.pats
       Fmt.(list ~sep:comma Pattern.pp)
       t.checks Ground.ClosedQuantifier.pp t.form
 end
@@ -78,41 +81,112 @@ let compute_top_triggers (cq : Ground.ClosedQuantifier.t) =
   let pats = CCList.sort_uniq ~cmp:Expr.Term.compare (aux [] t) in
   let tyvs = Expr.Ty.Var.S.of_list tyvs in
   let tvs = Expr.Term.Var.S.of_list tvs in
-  let pats_full, pats_partial =
-    Base.List.partition_tf
+  let pats =
+    Base.List.map
       ~f:(fun pat ->
         let sty, st =
           Expr.Term.free_vars (Expr.Ty.Var.S.empty, Expr.Term.Var.S.empty) pat
         in
+        let pat = Pattern.of_term ~subst:cq'.subst pat in
+        (pat, sty, st))
+      pats
+  in
+  let pats_full, pats_partial =
+    Base.List.partition_tf
+      ~f:(fun (_, sty, st) ->
         Expr.Ty.Var.S.subset tyvs sty && Expr.Term.Var.S.subset tvs st)
       pats
   in
-  let pats_full = List.map (Pattern.of_term ~subst:cq'.subst) pats_full in
-  let pats_partial = List.map (Pattern.of_term ~subst:cq'.subst) pats_partial in
-  let multi_pats =
-    let rec aux acc other = function
+  (* eliminate pattern variable *)
+  let pats_partial =
+    List.filter
+      (function Pattern.Var _, _, _ -> false | _ -> true)
+      pats_partial
+  in
+  let get_pat = List.map (fun (pat, _, _) -> pat) in
+  if Base.List.is_empty pats_full then (
+    (* compute smallest subsets of pats_partial that binds all the variables *)
+    let rec aux acc pats_candidate remaining_sty remaining_st = function
       | [] -> acc
-      | a :: l ->
-          aux
-            ({
-               pat = a;
-               checks = other @ l @ pats_partial;
-               form = cq;
-               eager = true;
-             }
-             :: acc)
-            (a :: other) l
+      | (pat, sty, st) :: pats_partial ->
+          if
+            Expr.Ty.Var.S.disjoint remaining_sty sty
+            && Expr.Term.Var.S.disjoint remaining_st st
+          then aux acc pats_candidate remaining_sty remaining_st pats_partial
+          else
+            let acc =
+              aux acc pats_candidate remaining_sty remaining_st pats_partial
+            in
+            let remaining_sty = Expr.Ty.Var.S.diff remaining_sty sty in
+            let remaining_st = Expr.Term.Var.S.diff remaining_st st in
+            if
+              Expr.Ty.Var.S.is_empty remaining_sty
+              && Expr.Term.Var.S.is_empty remaining_st
+            then (pat :: pats_candidate) :: acc
+            else
+              aux acc (pat :: pats_candidate) remaining_sty remaining_st
+                pats_partial
     in
-    aux [] [] pats_full
-  in
-  Debug.dprintf6 debug "@[pats_full:%a,@ pats_partial:%a,@ tri:%a@]@."
-    Fmt.(list ~sep:comma Pattern.pp)
-    pats_full
-    Fmt.(list ~sep:comma Pattern.pp)
-    pats_partial
-    Fmt.(list ~sep:comma pp)
-    multi_pats;
-  multi_pats
+    let full_subsets = aux [] [] tyvs tvs pats_partial in
+    let full_subsets =
+      Base.List.sort full_subsets ~compare:(fun l m ->
+          Int.compare (List.length l) (List.length m))
+    in
+    let full_subsets = Base.List.take full_subsets 4 in
+    let pats_partial = get_pat pats_partial in
+    let pats_full_with_others =
+      let rec aux acc other = function
+        | [] -> acc
+        | a :: l ->
+            aux
+              ({
+                 pat = a;
+                 pats = other @ l;
+                 checks = pats_partial;
+                 form = cq;
+                 eager = true;
+               }
+               :: acc)
+              (a :: other) l
+      in
+      List.concat_map (fun pats -> aux [] [] pats) full_subsets
+    in
+    Debug.dprintf4 debug
+      "@[@[<hv>no pats_full,@ @[pats_partial:%a@],@ @[tri:%a@]@]@]@."
+      Fmt.(list ~sep:comma Pattern.pp)
+      pats_partial
+      Fmt.(list ~sep:comma (hovbox pp))
+      pats_full_with_others;
+    pats_full_with_others)
+  else
+    let pats_full = get_pat pats_full in
+    let pats_partial = get_pat pats_partial in
+    let pats_full_with_others =
+      let rec aux acc other = function
+        | [] -> acc
+        | a :: l ->
+            aux
+              ({
+                 pat = a;
+                 pats = [];
+                 checks = other @ l @ pats_partial;
+                 form = cq;
+                 eager = true;
+               }
+               :: acc)
+              (a :: other) l
+      in
+
+      aux [] [] pats_full
+    in
+    Debug.dprintf6 debug "@[pats_full:%a,@ pats_partial:%a,@ tri:%a@]@."
+      Fmt.(list ~sep:comma Pattern.pp)
+      pats_full
+      Fmt.(list ~sep:comma Pattern.pp)
+      pats_partial
+      Fmt.(list ~sep:comma pp)
+      pats_full_with_others;
+    pats_full_with_others
 
 let compute_all_triggers (cq : Ground.ClosedQuantifier.t) =
   let cq' = Ground.ClosedQuantifier.sem cq in
@@ -161,6 +235,7 @@ let compute_all_triggers (cq : Ground.ClosedQuantifier.t) =
           Some
             {
               pat = Pattern.of_term ~subst:cq'.subst c;
+              pats = [];
               form = cq;
               eager = true;
               checks = [];
@@ -176,26 +251,31 @@ let get_user_triggers (cq : Ground.ClosedQuantifier.t) =
   let tyvs = Expr.Ty.Var.S.of_list cq'.ty_vars in
   let tvs = Expr.Term.Var.S.of_list cq'.term_vars in
   let pats =
-    List.filter_map
-      (function
-        | [ pat ] ->
-            let sty, st =
-              Expr.Term.free_vars
-                (Expr.Ty.Var.S.empty, Expr.Term.Var.S.empty)
-                pat
-            in
-            if Expr.Ty.Var.S.subset tyvs sty && Expr.Term.Var.S.subset tvs st
-            then
-              Some
-                {
-                  pat = Pattern.of_term ~subst:cq'.subst pat;
-                  form = cq;
-                  eager = true;
-                  checks = [];
-                }
-            else None
-        | _ -> None (* TODO: user multipattern *))
-      pats
+    Base.List.concat_map pats ~f:(fun pats ->
+        let sty, st =
+          List.fold_left
+            (fun acc pat -> Expr.Term.free_vars acc pat)
+            (Expr.Ty.Var.S.empty, Expr.Term.Var.S.empty)
+            pats
+        in
+        if Expr.Ty.Var.S.subset tyvs sty && Expr.Term.Var.S.subset tvs st then
+          let pats = List.map (Pattern.of_term ~subst:cq'.subst) pats in
+          let rec aux acc other = function
+            | [] -> acc
+            | a :: l ->
+                aux
+                  ({
+                     pat = a;
+                     pats = other @ l;
+                     checks = [];
+                     form = cq;
+                     eager = true;
+                   }
+                   :: acc)
+                  (a :: other) l
+          in
+          aux [] [] pats
+        else [])
   in
   pats
 
@@ -239,7 +319,9 @@ module Delayed_instantiation = struct
   let run d (tri, subst) =
     Debug.dprintf8 debug
       "[Quant] %a delayed instantiation %a, pat %a, checks:%a" Ground.Subst.pp
-      subst Ground.ClosedQuantifier.pp tri.form Pattern.pp tri.pat
+      subst Ground.ClosedQuantifier.pp tri.form
+      Fmt.(list ~sep:comma Pattern.pp)
+      tri.pats
       Fmt.(list ~sep:comma Pattern.pp)
       tri.checks;
     instantiate_aux d tri subst
@@ -256,7 +338,9 @@ let instantiate d tri subst =
     }
   in
   Debug.dprintf8 debug "[Quant] %a instantiation found %a, pat %a, checks:%a"
-    Ground.Subst.pp subst Ground.ClosedQuantifier.pp tri.form Pattern.pp tri.pat
+    Ground.Subst.pp subst Ground.ClosedQuantifier.pp tri.form
+    Fmt.(list ~sep:comma Pattern.pp)
+    tri.pats
     Fmt.(list ~sep:comma Pattern.pp)
     tri.checks;
   if
@@ -273,4 +357,9 @@ let instantiate d tri subst =
 let match_ d tri n =
   Debug.dprintf4 debug "[Quant] match %a %a" pp tri Node.pp n;
   let mvar = Pattern.match_term d Ground.Subst.S.empty n tri.pat in
+  let mvar =
+    List.fold_left
+      (fun acc pat -> Pattern.match_any_term d acc pat)
+      mvar tri.pats
+  in
   Ground.Subst.S.iter (fun subst -> instantiate d tri subst) mvar
diff --git a/src_colibri2/theories/quantifier/trigger.mli b/src_colibri2/theories/quantifier/trigger.mli
index 990e197025200839e379becb2926cbb3356d0c11..3299fe2f1b42a1c64565f1515a8b2d600f903755 100644
--- a/src_colibri2/theories/quantifier/trigger.mli
+++ b/src_colibri2/theories/quantifier/trigger.mli
@@ -21,8 +21,9 @@
 (** Trigger *)
 
 type t = {
-  pat : Pattern.t;
-      (** The main pattern, the one matched to obtain a complete
+  pat : Pattern.t;  (** The pattern on which to wait for a substitution *)
+  pats : Pattern.t list;
+      (** The other ones used to obtain a complete
                      substitution *)
   checks : Pattern.t list;  (** Guards for the existence of terms *)
   form : Ground.ClosedQuantifier.t;  (** the body of the formula *)
diff --git a/src_common/union.mlw b/src_common/union.mlw
index 1a023d3f9cbc816eb87a47f8d0caa2f619f6ce91..2cfd4dcb5ac50dee4f9b99ac9a4c392eabab7468 100644
--- a/src_common/union.mlw
+++ b/src_common/union.mlw
@@ -84,7 +84,7 @@ module Union
 
   type t' = { a: t }
    invariant {
-     forall i j. 0 <= i < j < length a -> Q.(nth i a < nth j a)
+     forall i j [nth i a,nth j a]. 0 <= i < j < length a -> Q.(nth i a < nth j a)
      }
    invariant {
      a <> Finite End
@@ -115,7 +115,7 @@ module Union
      | Finite l ->
        mem0 x l
      | Inf ->
-       false
+       true
      end
 
    let singleton (q:Q.t) : t'
@@ -134,19 +134,27 @@ module Union
       match u.a with
       | Inf -> (None, ghost 0., ghost 1.)
       | InfFinite q _ _ -> (None, ghost (Q.real q)-.1., ghost (Q.real q)-.2.)
-      | Finite (Singleton q End) -> (Some q,0., 1.)
+      | Finite (Singleton q End) ->
+    
+      assert { forall x:real. mem x u.a -> mem0 x (Singleton q End) };
+      assert { forall x:real. mem x u.a -> (x = q \/ mem0 x End) };
+      assert { forall x:real. mem0 x End -> false };
+       (Some q,0., 1.)
       | Finite End -> absurd
       | Finite (Inter q b q' b' _) ->
-        assert { length u.a >= 2 };
         assert { nth 0 u.a = q };
         assert { nth 1 u.a = q' };
         assert { (Q.real q) <. (Q.real q') };
         (None, ghost (Q.real q)*.0.75+.(Q.real q')*.0.25, ghost (Q.real q)*.0.25+.(Q.real q')*.0.75)
       | Finite (FiniteInf q _) -> (None,ghost (Q.real q)+.1.,ghost (Q.real q)+.2.)
       | Finite (Singleton q (Singleton q' _)) ->
+        assert { nth 0 u.a = q };
+        assert { nth 1 u.a = q' };
         assert { (Q.real q) <. (Q.real q') };
         (None,ghost (Q.real q), ghost (Q.real q'))
       | Finite (Singleton _ (Inter q b q' b' _)) ->
+        assert { nth 1 u.a = q };
+        assert { nth 2 u.a = q' };
         assert { (Q.real q) <. (Q.real q') };
         (None, ghost (Q.real q)*.0.75+.(Q.real q')*.0.25, ghost (Q.real q)*.0.25+.(Q.real q')*.0.75)
       | Finite (Singleton _ (FiniteInf q _)) -> (None,ghost (Q.real q)+.1.,ghost (Q.real q)+.2.)
diff --git a/src_common/union/why3session.xml b/src_common/union/why3session.xml
index bead75ff46fa09799b93f9caa03223cc37813917..b20a311776eafbb51036e5477ba91030a42dfa84 100644
--- a/src_common/union/why3session.xml
+++ b/src_common/union/why3session.xml
@@ -23,10 +23,25 @@
  <proof prover="3"><result status="valid" time="2.82"/></proof>
  </goal>
  <goal name="is_singleton&#39;vc" expl="VC for is_singleton">
- <proof prover="3" obsolete="true"><result status="highfailure" time="0.02"/></proof>
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
  <transf name="split_vc" >
-  <goal name="is_singleton&#39;vc.0" expl="assertion">
+  <goal name="is_singleton&#39;vc.0" expl="assertion" proved="true">
   <proof prover="3"><result status="timeout" time="5.00"/></proof>
+  <transf name="instantiate" proved="true" arg1="t&#39;&#39;invariant" arg2="u">
+   <goal name="is_singleton&#39;vc.0.0" expl="assertion" proved="true">
+   <proof prover="3"><result status="timeout" time="5.00"/></proof>
+   <transf name="destruct" proved="true" arg1="Hinst">
+    <goal name="is_singleton&#39;vc.0.0.0" expl="assertion" proved="true">
+    <proof prover="3" obsolete="true"><path name="union-Union-is_singletonqtvc_3.psmt2"/><result status="timeout" time="5.00"/></proof>
+    <transf name="instantiate" proved="true" arg1="Hinst1" arg2="0,1">
+     <goal name="is_singleton&#39;vc.0.0.0.0" expl="assertion" proved="true">
+     <proof prover="3"><result status="valid" time="0.97"/></proof>
+     </goal>
+    </transf>
+    </goal>
+   </transf>
+   </goal>
+  </transf>
   </goal>
   <goal name="is_singleton&#39;vc.1" expl="assertion">
   <proof prover="3"><result status="timeout" time="5.00"/></proof>
@@ -34,22 +49,37 @@
   <goal name="is_singleton&#39;vc.2" expl="unreachable point" proved="true">
   <proof prover="3"><result status="valid" time="0.03"/></proof>
   </goal>
-  <goal name="is_singleton&#39;vc.3" expl="assertion">
+  <goal name="is_singleton&#39;vc.3" expl="assertion" proved="true">
+  <proof prover="3"><result status="valid" time="0.03"/></proof>
   </goal>
   <goal name="is_singleton&#39;vc.4" expl="assertion" proved="true">
-  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="is_singleton&#39;vc.5" expl="assertion" proved="true">
-  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  <proof prover="3"><result status="valid" time="0.03"/></proof>
   </goal>
-  <goal name="is_singleton&#39;vc.6" expl="assertion">
+  <goal name="is_singleton&#39;vc.6" expl="assertion" proved="true">
   <proof prover="3"><result status="timeout" time="5.00"/></proof>
+  <transf name="instantiate" proved="true" arg1="t&#39;&#39;invariant" arg2="u">
+   <goal name="is_singleton&#39;vc.6.0" expl="assertion" proved="true">
+   <transf name="destruct" proved="true" arg1="Hinst">
+    <goal name="is_singleton&#39;vc.6.0.0" expl="assertion" proved="true">
+    <proof prover="3" obsolete="true"><path name="union-Union-is_singletonqtvc_4.psmt2"/><result status="timeout" time="5.00"/></proof>
+    <transf name="instantiate" proved="true" arg1="Hinst1" arg2="0,1">
+     <goal name="is_singleton&#39;vc.6.0.0.0" expl="assertion" proved="true">
+     <proof prover="3"><result status="valid" time="0.03"/></proof>
+     </goal>
+    </transf>
+    </goal>
+   </transf>
+   </goal>
+  </transf>
   </goal>
   <goal name="is_singleton&#39;vc.7" expl="postcondition">
   <proof prover="3" obsolete="true"><result status="highfailure" time="0.05"/></proof>
   <transf name="split_vc" >
-   <goal name="is_singleton&#39;vc.7.0" expl="postcondition" proved="true">
-   <proof prover="3"><result status="valid" time="0.57"/></proof>
+   <goal name="is_singleton&#39;vc.7.0" expl="postcondition">
+   <proof prover="3"><result status="timeout" time="5.00"/></proof>
    </goal>
    <goal name="is_singleton&#39;vc.7.1" expl="postcondition" proved="true">
    <proof prover="3"><result status="valid" time="0.08"/></proof>
@@ -67,16 +97,16 @@
     <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="is_singleton&#39;vc.7.2.3" expl="postcondition" proved="true">
-    <proof prover="3"><result status="valid" time="0.02"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_singleton&#39;vc.7.2.4" expl="postcondition" proved="true">
-    <proof prover="3"><result status="valid" time="0.02"/></proof>
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
     </goal>
     <goal name="is_singleton&#39;vc.7.2.5" expl="postcondition" proved="true">
     <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="is_singleton&#39;vc.7.2.6" expl="postcondition" proved="true">
-    <proof prover="3"><result status="valid" time="0.01"/></proof>
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="is_singleton&#39;vc.7.2.7" expl="postcondition" proved="true">
     <proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -87,7 +117,7 @@
    <proof prover="3" obsolete="true"><result status="unknown" time="0.01"/></proof>
    <transf name="split_vc" >
     <goal name="is_singleton&#39;vc.7.3.0" expl="postcondition">
-    <proof prover="3"><result status="unknown" time="0.04"/></proof>
+    <proof prover="3"><result status="unknown" time="0.31"/></proof>
     </goal>
     <goal name="is_singleton&#39;vc.7.3.1" expl="postcondition" proved="true">
     <proof prover="3"><result status="valid" time="0.05"/></proof>
@@ -98,14 +128,14 @@
     <goal name="is_singleton&#39;vc.7.3.3" expl="postcondition" proved="true">
     <proof prover="3"><result status="valid" time="0.03"/></proof>
     </goal>
-    <goal name="is_singleton&#39;vc.7.3.4" expl="postcondition">
-    <proof prover="3"><result status="timeout" time="5.00"/></proof>
+    <goal name="is_singleton&#39;vc.7.3.4" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.13"/></proof>
     </goal>
     <goal name="is_singleton&#39;vc.7.3.5" expl="postcondition" proved="true">
     <proof prover="3"><result status="valid" time="0.60"/></proof>
     </goal>
     <goal name="is_singleton&#39;vc.7.3.6" expl="postcondition" proved="true">
-    <proof prover="3"><result status="valid" time="0.09"/></proof>
+    <proof prover="3"><result status="valid" time="0.05"/></proof>
     </goal>
     <goal name="is_singleton&#39;vc.7.3.7" expl="postcondition" proved="true">
     <proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -116,7 +146,7 @@
    <proof prover="3" obsolete="true"><result status="unknown" time="0.01"/></proof>
    <transf name="split_vc" >
     <goal name="is_singleton&#39;vc.7.4.0" expl="postcondition">
-    <proof prover="3"><result status="unknown" time="0.04"/></proof>
+    <proof prover="3"><result status="unknown" time="0.30"/></proof>
     </goal>
     <goal name="is_singleton&#39;vc.7.4.1" expl="postcondition" proved="true">
     <proof prover="3"><result status="valid" time="0.03"/></proof>
@@ -125,16 +155,16 @@
     <proof prover="3"><result status="valid" time="0.02"/></proof>
     </goal>
     <goal name="is_singleton&#39;vc.7.4.3" expl="postcondition" proved="true">
-    <proof prover="3"><result status="valid" time="0.62"/></proof>
+    <proof prover="3"><result status="valid" time="0.10"/></proof>
     </goal>
-    <goal name="is_singleton&#39;vc.7.4.4" expl="postcondition">
-    <proof prover="3"><result status="timeout" time="5.00"/></proof>
+    <goal name="is_singleton&#39;vc.7.4.4" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.12"/></proof>
     </goal>
     <goal name="is_singleton&#39;vc.7.4.5" expl="postcondition" proved="true">
     <proof prover="3"><result status="valid" time="0.67"/></proof>
     </goal>
     <goal name="is_singleton&#39;vc.7.4.6" expl="postcondition" proved="true">
-    <proof prover="3"><result status="valid" time="0.08"/></proof>
+    <proof prover="3"><result status="valid" time="0.06"/></proof>
     </goal>
     <goal name="is_singleton&#39;vc.7.4.7" expl="postcondition" proved="true">
     <proof prover="3"><result status="valid" time="0.03"/></proof>