diff --git a/Src/COLIBRI/arith.pl b/Src/COLIBRI/arith.pl
index ba424247751dc60dbd478cb18470417e149fb310..be17f34c658efc8141f246807ac8af4b3ff6ae8c 100755
--- a/Src/COLIBRI/arith.pl
+++ b/Src/COLIBRI/arith.pl
@@ -6932,6 +6932,7 @@ mult_intervals_diff_both_both(Min1,Max1,Min2,Max2,B1,B2) :-
 %%                 GESTION DES CONGRUENCES
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 :- export launch_congr/3.
+%launch_congr(A,C0,Mod0) :- !.
 launch_congr(A,C0,Mod0) :-
     (launch_congr1(A,C0,Mod0) ->
         true
diff --git a/Src/COLIBRI/smt_import.pl b/Src/COLIBRI/smt_import.pl
index 4dc76a9a0ab3a3f7f591e7b30d5a92e840a1841c..4aa3320d4688ee7cbb94129ac4d08a825ce05ac8 100644
--- a/Src/COLIBRI/smt_import.pl
+++ b/Src/COLIBRI/smt_import.pl
@@ -1381,7 +1381,10 @@ defined_smt_func(F/Ar,IArgs,Type,IExpr) :-
          foreach(CFV,CFVars),
          fromto(VarsAss,OVA,IVA,[]),
          param(LetVars) do
-            (occurs(FV,LetVars) ->
+            % pas d'unification plus tard !
+            ((occurs(FV,LetVars);
+              is_quantifier_abstraction(FV))
+            ->
                 OVA = IVA
             ;   OVA = [[FV|CFV]|IVA])),
         (foreach((IArg,IArgType),IArgs),
@@ -2902,6 +2905,10 @@ new_quantifier_abstraction(Res) :-
     setval(decl,ODecl-NEnd),
     Res = as(NVar,bool).
 
+is_quantifier_abstraction(Var) :-
+    protected_get_var_name(Var,VS),
+    append_strings("ColQuant",_,VS).
+    
 % on garde les realString
 check_eval(Type,realString(Str),RE) ?- !,
     RE = as(realString(Str),Type).
diff --git a/tests/sat/zero_neg_plus.smt2 b/tests/sat/zero_neg_plus.smt2
deleted file mode 100644
index 4e39c693fda8a512e856325e12d3e18cd0c0e70e..0000000000000000000000000000000000000000
--- a/tests/sat/zero_neg_plus.smt2
+++ /dev/null
@@ -1,18 +0,0 @@
-(set-info :status sat)
-;; produced by colibri.drv ;;
-(set-logic ALL)
-(set-info :smt-lib-version 2.6)
-
-(declare-const zero_plus Float32)
-
-(declare-const zero_neg Float32)
-
-(declare-fun magic (Float32) Int)
-
-(assert (fp.eq zero_plus zero_neg))
-
-(assert (distinct (magic zero_neg) 0))
-
-(assert (not (not (= (magic zero_plus) 0))))
-
-(check-sat)
diff --git a/tests/unknown/bool_eq.smt2 b/tests/unknown/bool_eq.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..56834b15debef094d7f3eda95e14ae00577646e5
--- /dev/null
+++ b/tests/unknown/bool_eq.smt2
@@ -0,0 +1,28 @@
+;; produced by colibri.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+;; sat normalement mais unknown à cause du forall
+
+;; bool_eq
+(define-fun bool_eq ((arg1 (Array Int Bool)) (a__first Int) (a__last Int) (b (Array Int Bool)) (b__first Int) (b__last Int)) Bool
+  (and
+         (ite (<= a__first a__last)
+           (and
+             (<= b__first b__last)
+             (= (- a__last a__first) (- b__last b__first)))
+           (< b__last b__first))
+         (forall ((idx Int))
+           (=>
+             (and (<= a__first idx) (<= idx a__last))
+             (= (ite (select arg1 idx) 1 0) (ite (select b (+ (- b__first a__first) idx)) 1 0))))))
+
+
+(declare-const a (Array Int Bool))
+(declare-const b (Array Int Bool))
+(declare-const c (Array Int Bool))
+
+(assert (not (bool_eq c 0 1 a 0 1)))
+(assert (bool_eq b 0 1 c 0 1))
+
+
+(check-sat)
diff --git a/tests/unsat/bool_eq_unsat.smt2 b/tests/unsat/bool_eq_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..9c1bf81aa6c5c70898defd10eccd875d704f8a2a
--- /dev/null
+++ b/tests/unsat/bool_eq_unsat.smt2
@@ -0,0 +1,28 @@
+(set-info :status unsat)
+;; produced by colibri.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+
+;; bool_eq
+(define-fun bool_eq ((arg1 (Array Int Bool)) (a__first Int) (a__last Int) (b (Array Int Bool)) (b__first Int) (b__last Int)) Bool
+  (and
+         (ite (<= a__first a__last)
+           (and
+             (<= b__first b__last)
+             (= (- a__last a__first) (- b__last b__first)))
+           (< b__last b__first))
+         (forall ((idx Int))
+           (=>
+             (and (<= a__first idx) (<= idx a__last))
+             (= (ite (select arg1 idx) 1 0) (ite (select b (+ (- b__first a__first) idx)) 1 0))))))
+
+
+(declare-const a (Array Int Bool))
+(declare-const b (Array Int Bool))
+(declare-const c (Array Int Bool))
+
+(assert (not (bool_eq c 0 1 a 0 1)))
+(assert (bool_eq c 0 1 a 0 1))
+
+
+(check-sat)