diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index 999742df7ebca651a2883f7c18c474166e1b4349..1d4b80cfd0734aaea6a9547caac89fba589052a2 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -841,15 +841,14 @@ smt_test(TO,Size) :-
%StrDir = "./QF_ABVFP/20170428-Liew-KLEE/aachen_real_gmp_gmp_klee_mul.x86_64/", % 3 (bitwuzla 0)
%StrDir = "QF_ABVFP/20170428-Liew-KLEE/aachen_real_numerical_recipes_qrdcmp.x86_64/",
- StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 109 (177 unsupported) (cvc4 55)
- %StrDir = "./QF_ABVFP/20170501-Heizmann-UltimateAutomizer/", % 1
- % min_solve (cvc4 0) OK
+ %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 100 (177 unsupported) (cvc4 55)
+ %StrDir = "./QF_ABVFP/20170501-Heizmann-UltimateAutomizer/", % 0 min_solve (cvc4 0) OK
%----------------------------------------------------------------------
- %StrDir = "./QF_ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/",% 2 (cvc4 1|2)!
+ %StrDir = "./QF_ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/",% 0 (cvc4 1|2)!
%StrDir = "./QF_ABVFPLRA/20170501-Heizmann-UltimateAutomizer/",% 0 (0)
%--------------------------------------------------------------------------
%StrDir = "./QF_BVFP/20170428-Liew-KLEE/aachen_real_numerical_recipes_qrdcmp.x86_64/",
- %StrDir = "./QF_BVFP/20170428-Liew-KLEE/imperial_synthetic_sqrt_klee.x86_64//",
+ %StrDir = "./QF_BVFP/20170428-Liew-KLEE/imperial_synthetic_sqrt_klee.x86_64/", % 3 (bitwuzla 3)
%StrDir = "./QF_BVFP/20170428-Liew-KLEE/aachen_syn_halve_longdouble-flow.x86_64/",% 4u
%StrDir = "./QF_BVFP/20170428-Liew-KLEE/", % 16 (cvc4 50)(bitwuzla
@@ -872,7 +871,7 @@ 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/", % 43/46 (min_solve, sans lin_solve ni ls_reduce..)(39)
+ StrDir = "./QF_FP/griggio/", % 50 (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/wintersteiger/", % tout OK
diff --git a/Src/COLIBRI/mbv_propa.pl b/Src/COLIBRI/mbv_propa.pl
index 215b8205fc1e75f67db0515bb1a8e0012fd17e40..52eaf4e65fe523c430419dc2ede7a7286f14c94d 100644
--- a/Src/COLIBRI/mbv_propa.pl
+++ b/Src/COLIBRI/mbv_propa.pl
@@ -154,11 +154,10 @@ update_congr_interval_eq(X,Y):-
% EN TEST: ca marche !!!
-/*
launch_bveq(Sx,X,Sy,Y) :-
!,
protected_unify(X,Y).
-*/
+
launch_bveq(S,X,S,Y) ?- !,
protected_unify(X,Y).
launch_bveq(Sx,X,Sy,Y) :-
diff --git a/Src/COLIBRI/realarith.pl b/Src/COLIBRI/realarith.pl
index 5ba31be26e435784d34006d6e1d5d695ebd5caa7..76217f8eecfe2361174db0226e7a9aa66f6cc1c7 100755
--- a/Src/COLIBRI/realarith.pl
+++ b/Src/COLIBRI/realarith.pl
@@ -4471,7 +4471,8 @@ real_inter_dom_if_eq(_,_,DomA,DomB,DomC,DomA,DomB,DomC).
-
+% BUG
+reduce_dom_add_args_from_res(_,Type,FIA,FIB,FIC,RelCA,RelCB,DomA,DomB,DomC,DomA,DomB) :- !.
reduce_dom_add_args_from_res(0,Type,FIA,FIB,FIC,RelCA,RelCB,DomA,DomB,DomC,DomA,DomB) :- !.
reduce_dom_add_args_from_res(1,Type,FIA,FIB,FIC,RelCA,RelCB,DomA0,DomB0,DomC,DomA,DomB) :-
mreal:dom_interval(DomA0,IA0),
@@ -9348,40 +9349,42 @@ minus_float_rec(0,1,Type,A,B,C) :- !,
writeln(output,max_iter:minus_float_rec(A,B,C))
; true).
minus_float_rec(Cpt,RS,Type,A,B,C) :-
- mreal:dvar_domain(A,DomA0),
- mreal:dvar_domain(B,DomB0),
- mreal:dvar_domain(C,DomC),
- (RS == 1 ->
- get_rel_between_real_args(A,B,RelAB),
- get_rel_between_real_args(C,B,RelCB),
- get_rel_between_real_args(A,C,RelAC),
- get_float_int_status(A,FIA),
- get_float_int_status(B,FIB),
- get_float_int_status(C,FIC)
- ; (RelAB,RelCB,RelAC) = (?,?,?),
- (FIA,FIB,FIC) = (0,0,0)),
- %% On reduit les domaines de A et B par les proprietes de
- %% NON CANCELATION (C <> 0) et NON ABSORBTION (A <> C)
- reduce_dom_minus_args_from_res(RS,Type,FIA,FIB,FIC,RelAC,DomA0,DomB0,DomC,DomA,DomB),
- %% Si C instancie et non nul on peut avoir une convergence tres lente
- %% (ex: minus_real(A,B,2.1))
- %% On utilise donc un compteur pour limiter les iterations de
- %% minus_float_rec
- minus_float_rec(RS,3,Type,FIA,FIB,FIC,DomA,DomB,DomC,RelAB,RelCB,RelAC,NDomA,NDomB,NDomC),
- mreal:dvar_set(A,NDomA),
- mreal:dvar_set(B,NDomB),
- mreal:dvar_set(C,NDomC),
- (RS == 1 ->
- mreal:dvar_domain(A,NewDomA),
- mreal:dvar_domain(B,NewDomB),
- mreal:dvar_domain(C,NewDomC),
- % = necessaire
- ((NDomA,NDomB,NDomC) = (NewDomA,NewDomB,NewDomC) ->
- true
- ; NCpt is Cpt - 1,
- minus_float_rec(NCpt,RS,Type,A,B,C))
- ; true).
-
+ mreal:dvar_domain(A,DomA0),
+ mreal:dvar_domain(B,DomB0),
+ mreal:dvar_domain(C,DomC),
+ (RS == 1 ->
+ get_rel_between_real_args(A,B,RelAB),
+ get_rel_between_real_args(C,B,RelCB),
+ get_rel_between_real_args(A,C,RelAC),
+ get_float_int_status(A,FIA),
+ get_float_int_status(B,FIB),
+ get_float_int_status(C,FIC)
+ ; (RelAB,RelCB,RelAC) = (?,?,?),
+ (FIA,FIB,FIC) = (0,0,0)),
+ % On reduit les domaines de A et B par les proprietes de
+ % NON CANCELATION (C <> 0) et NON ABSORBTION (A <> C)
+ reduce_dom_minus_args_from_res(RS,Type,FIA,FIB,FIC,RelAC,DomA0,DomB0,DomC,DomA,DomB),
+ % Si C instancie et non nul on peut avoir une convergence tres lente
+ % (ex: minus_real(A,B,2.1))
+ % On utilise donc un compteur pour limiter les iterations de
+ % minus_float_rec
+ minus_float_rec(RS,3,Type,FIA,FIB,FIC,DomA,DomB,DomC,RelAB,RelCB,RelAC,NDomA,NDomB,NDomC),
+ mreal:dvar_set(A,NDomA),
+ mreal:dvar_set(B,NDomB),
+ mreal:dvar_set(C,NDomC),
+ (RS == 1 ->
+ mreal:dvar_domain(A,NewDomA),
+ mreal:dvar_domain(B,NewDomB),
+ mreal:dvar_domain(C,NewDomC),
+ % = necessaire
+ ((NDomA,NDomB,NDomC) = (NewDomA,NewDomB,NewDomC) ->
+ true
+ ; NCpt is Cpt - 1,
+ minus_float_rec(NCpt,RS,Type,A,B,C))
+ ; true).
+
+% BUG
+reduce_dom_minus_args_from_res(_,_,FIA,FIB,FIC,RelAC,DomA,DomB,DomC,DomA,DomB) :- !.
reduce_dom_minus_args_from_res(0,_,FIA,FIB,FIC,RelAC,DomA,DomB,DomC,DomA,DomB) :- !.
reduce_dom_minus_args_from_res(1,Type,FIA,FIB,FIC,RelAC,DomA0,DomB0,DomC,DomA,DomB) :-
mreal:dom_interval(DomA0,IA0),