Import from Bin:a1af7a0 Src:a835b4644 farith:a93db57

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

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).