diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index 066b291bb7b4552f0597864c42c3da4b8f915aa0..baa838df33fccbdb09da9478b89b62fafeaad68a 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -449,35 +449,8 @@ test_colibri :-
     writeln(output,"NbSimplex":NbS).
 
 
-smt_solve_get_stat(FILE) :-
-    % On passe en mode comptage du nombre de steps
-    setval(step_stats,1)@eclipse,
-    % Si on a une limite elle est donnée dans la ligne de commande
-    (current_array(step_limit,_) ->
-        true
-    ;   setval(step_limit,0)@eclipse),
-    setval(nb_steps,0)@eclipse,
-    setval(simplex_steps,0)@eclipse,
-    smt_solve(_,FILE,0,Code),
-    (getval(show_steps,1)@eclipse ->
-        getval(nb_steps,Steps)@eclipse,
-        writeln(output,"Steps":Steps)
-    ;   true),
-    exit(Code).
-
-smt_solve_with_step_limit(FILE) :-
-    % On passe en mode comptage du nombre de steps
-    setval(step_stats,1)@eclipse,
-    setval(show_steps,1)@eclipse,
-    % Si on a une limite elle est donnée dans la ligne de commande
-    (current_array(step_limit,_) ->
-        true
-    ;   setval(step_limit,0)@eclipse),
-    setval(nb_steps,0)@eclipse,
-    setval(simplex_steps,0)@eclipse,
-    smt_solve(_,FILE,0,Code),
-    exit(Code).
 
+/*
 smt_solve_count_steps(FILE,TO) :-
     setval(show_steps,1)@eclipse,
     getval(use_delta,UD)@eclipse,
@@ -502,7 +475,7 @@ smt_solve_count_steps(FILE,TO) :-
            exit_block(Tag))),
     setval(use_delta,UD)@eclipse,
     setval(use_simplex,US)@eclipse.
-
+*/
 
 smt_comp_solve(FILE) :-
     % pas de message sur error pour la smtcomp
@@ -521,11 +494,16 @@ smt_comp_solve(FILE) :-
 
 smt_solve(FILE) :-
     % Pas de désactivation du simples apres DDSteps
-    DDSteps = 0,
-    setval(simplex_delay_deactivation,DDSteps)@eclipse,
-    % Pas de comptage de steps
-    setval(step_stats,0)@eclipse,
-    setval(step_limit,0)@eclipse,
+    % (5000 par défaut dans colibri.pl)
+    % DDSteps = 0,
+    % setval(simplex_delay_deactivation,DDSteps)@eclipse,
+
+    % On passe en mode comptage du nombre de steps
+    setval(step_stats,1)@eclipse,
+    % Si on a une limite elle est donnée dans la ligne de commande
+    (current_array(step_limit,_) ->
+        true
+    ;   setval(step_limit,0)@eclipse),
     setval(nb_steps,0)@eclipse,
     setval(simplex_steps,0)@eclipse,
     % on active les warning de dolmen
@@ -533,6 +511,20 @@ smt_solve(FILE) :-
     smt_solve(_,FILE,0,Code),
     exit(Code).
 
+smt_solve_get_stat(FILE) :-
+    % On passe en mode comptage du nombre de steps
+    setval(step_stats,1)@eclipse,
+    % Si on a une limite elle est donnée dans la ligne de commande
+    (current_array(step_limit,_) ->
+        true
+    ;   setval(step_limit,0)@eclipse),
+    setval(nb_steps,0)@eclipse,
+    setval(simplex_steps,0)@eclipse,
+    smt_solve(_,FILE,0,Code),
+    getval(nb_steps,Steps)@eclipse,
+    writeln(output,"Steps":Steps),
+    exit(Code).
+
 smt_solve(Test,FILE,TO,Code) :-
     no_3B,
     set_threshold(1e-3),
@@ -738,10 +730,10 @@ smt_test :-
 
 smt_test(TO,Size) :-
     %StrDir = "./colibri-master/tests/",
-    StrDir = "./colibri-master/tests/sat/", %0 (sans real/float-> int!)
+    %StrDir = "./colibri-master/tests/sat/", %0 (sans real/float-> int!)
     %StrDir = "./colibri-master/tests/unsat/", %0
     %StrDir = "./colibri-master/tests/unknown/",
-    %StrDir = "./colibri-master/tests/timeout/",
+    StrDir = "./colibri-master/tests/timeout/",
 
     %StrDir = "./smt/",
     %StrDir = "./AdaCore/",
@@ -876,9 +868,9 @@ smt_test(TO,Size) :-
     %StrDir = "./QF_FP/20170501-Heizmann-UltimateAutomizer/", % 0
     %StrDir = "./QF_FP/20190429-UltimateAutomizerSvcomp2019/",% 0 (bitwuzla 0)
     %StrDir = "./QF_FP/ramalho/", % 0 (cvc4 19)(bitwuzla 17)
-    %StrDir = "./QF_FP/griggio/", % 50 (min_solve, sans lin_solve ni ls_reduce..)(39)
+    %StrDir = "./QF_FP/griggio/", % 49 (min_solve, sans lin_solve ni ls_reduce..)(39)
     %(cvc4 89)(bitwuzla 74) LES DD DEMARRENT TROP VITE ?
-    %StrDir = "./QF_FP/schanda/spark/", % 6 (min_solve avec X =< (X+Y)/2 =< Y) (ncvc4 8)(bitwuzla 3)
+    %StrDir = "./QF_FP/schanda/spark/", % 6! (min_solve avec X =< (X+Y)/2 =< Y) (ncvc4 8)(bitwuzla 3)
     %StrDir = "./QF_FP/wintersteiger/", % tout OK
 %-----------------------------------------------------------------------    
     %StrDir = "./QF_UFFP/schanda/",% 0
@@ -1001,6 +993,7 @@ smt_test0(TO,Size,StrDir) :-
           os_file_name(OF,F),
           concat_string(["cmd.exe /D /C smt_test_file ",OF," ",TO],Com)
       ;   concat_string(["timeout --signal=KILL --kill-after=0.1 ",TO,"s ",ECLIPSE," -b ",COL," -g ",SizeM," -e \"seed(0),use_delta,use_simplex,setval(def_real_for_int,1)@colibri,setval(step_limit,0),setval(no_dolmen_warning,1)@eclipse,setval(show_steps,1),smt_solve_get_stat(\'",F,"\')\""],Com)),
+
 %      ;   concat_string(["timeout --signal=KILL --kill-after=0.1 ",TO,"s ",ECLIPSE," -b ",COL," -g ",SizeM," -e \"seed(0),smt_comp_solve(\'",F,"\')\""],Com)),
 
 %;          concat_string(["timeout --signal=KILL --kill-after=0.1 ",TO,"s cvc4 ",F],Com)),
diff --git a/Src/COLIBRI/solve.pl b/Src/COLIBRI/solve.pl
index de828fcfec23e2a8c14f2b4802f8fed8f4cbd469..e8e1313ac17952a6b389f2b7b19b286ab728498f 100644
--- a/Src/COLIBRI/solve.pl
+++ b/Src/COLIBRI/solve.pl
@@ -11153,10 +11153,13 @@ get_most_constrained_bool_var([(V,D,Adj)|UseList],VN,NUseList,Seen,OVar,ONb,Var,
               ;   (Type == rnd ->
                       true
                   ;   % A ANALYSER/GENERALISER AUX AUTRES TYPES
-                      % Bon sur ramalho +1
-                      % Mauvais sur les sat de colibri_test
-                      fail,
+                      % pas d'effet visible !
+                      % fail,
                       real_type(Type,_),
+                      mreal:get_intervals(E,EI),
+                      EI = [L,H],
+                      number(L),
+                      number(H),
                       mreal:dvar_size(E,2),
                       call(spy_here)@eclipse)),
               not occurs(E,ISeen))