diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 0a5c40dbd..1b0555b22 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -500,40 +500,40 @@ namespace qe {
         }
     }
 
-        class kernel {
-            ast_manager& m;
-            smt_params   m_smtp;
-            smt::kernel  m_kernel;
-            
-        public:
-            kernel(ast_manager& m):
-                m(m),
-                m_kernel(m, m_smtp)
-            {
-                m_smtp.m_model = true;
-                m_smtp.m_relevancy_lvl = 0;
-                m_smtp.m_case_split_strategy = CS_ACTIVITY_WITH_CACHE;
+    class kernel {
+        ast_manager& m;
+        smt_params   m_smtp;
+        smt::kernel  m_kernel;
+        
+    public:
+        kernel(ast_manager& m):
+            m(m),
+            m_kernel(m, m_smtp)
+        {
+            m_smtp.m_model = true;
+            m_smtp.m_relevancy_lvl = 0;
+            m_smtp.m_case_split_strategy = CS_ACTIVITY_WITH_CACHE;
+        }
+        
+        smt::kernel& k() { return m_kernel; }
+        smt::kernel const& k() const { return m_kernel; }
+        
+        void assert_expr(expr* e) {
+            m_kernel.assert_expr(e);
+        }
+        
+        void get_core(expr_ref_vector& core) {
+            unsigned sz = m_kernel.get_unsat_core_size();
+            core.reset();
+            for (unsigned i = 0; i < sz; ++i) {
+                core.push_back(m_kernel.get_unsat_core_expr(i));
             }
-            
-            smt::kernel& k() { return m_kernel; }
-            smt::kernel const& k() const { return m_kernel; }
-            
-            void assert_expr(expr* e) {
-                m_kernel.assert_expr(e);
-            }
-            
-            void get_core(expr_ref_vector& core) {
-                unsigned sz = m_kernel.get_unsat_core_size();
-                core.reset();
-                for (unsigned i = 0; i < sz; ++i) {
-                    core.push_back(m_kernel.get_unsat_core_expr(i));
-                }
-                TRACE("qe", tout << "core: " << core << "\n";
-                      m_kernel.display(tout);
-                      tout << "\n";
-                      );
-            }
-        };
+            TRACE("qe", tout << "core: " << core << "\n";
+                  m_kernel.display(tout);
+                  tout << "\n";
+                  );
+        }
+    };
     
     class qsat : public tactic {
         
@@ -1168,6 +1168,7 @@ namespace qe {
         pred_abs        m_pred_abs;
         qe::mbp         m_mbp;
         kernel          m_kernel;
+        vector<app_ref_vector> m_vars;
 
         imp(ast_manager& m): 
             m(m), 
@@ -1180,14 +1181,36 @@ namespace qe {
             m_fmls.push_back(e);
         }
 
-        lbool check(svector<bool> const& is_max, func_decl_ref_vector const& vars, app* t) {
+        lbool check(svector<bool> const& is_max, app_ref_vector const& vars, app* t) {
             // Assume this is the only call to check.
             expr_ref_vector defs(m);
+            app_ref_vector free_vars(m), vars1(m);
             expr_ref fml = mk_and(m_fmls);
+            m_pred_abs.get_free_vars(fml, free_vars);
             m_pred_abs.abstract_atoms(fml, defs);
             fml = m_pred_abs.mk_abstract(fml);
             m_kernel.assert_expr(mk_and(defs));
             m_kernel.assert_expr(fml);
+            obj_hashtable<app> var_set;
+            for (unsigned i = 0; i < vars.size(); ++i) {
+                var_set.insert(vars[i]);
+            }
+            for (unsigned i = 0; i < free_vars.size(); ++i) {
+                app* v = free_vars[i].get();
+                if (!var_set.contains(v)) {
+                    vars1.push_back(v);
+                }
+            }
+            bool is_m = is_max[0];
+            for (unsigned i = 0; i < vars.size(); ++i) {
+                if (is_m != is_max[i]) {
+                    m_vars.push_back(vars1);
+                    vars1.reset();       
+                    is_m = is_max[i];
+                }
+                vars1.push_back(vars[i]);
+            }
+
             // TBD
             
             return l_undef;
@@ -1212,7 +1235,7 @@ namespace qe {
         }
     }
 
-    lbool min_max_opt::check(svector<bool> const& is_max, func_decl_ref_vector const& vars, app* t) {
+    lbool min_max_opt::check(svector<bool> const& is_max, app_ref_vector const& vars, app* t) {
         return m_imp->check(is_max, vars, t);
     }
 
diff --git a/src/qe/qsat.h b/src/qe/qsat.h
index 91b370294..5c6b80a04 100644
--- a/src/qe/qsat.h
+++ b/src/qe/qsat.h
@@ -121,7 +121,7 @@ namespace qe {
         ~min_max_opt();
         void add(expr* e);
         void add(expr_ref_vector const& fmls);
-        lbool check(svector<bool> const& is_max, func_decl_ref_vector const& vars, app* t);
+        lbool check(svector<bool> const& is_max, app_ref_vector const& vars, app* t);
     };
 
 
diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h
index 72e1f1bc2..8f209b96b 100644
--- a/src/smt/theory_arith_int.h
+++ b/src/smt/theory_arith_int.h
@@ -1308,7 +1308,7 @@ namespace smt {
         if (!gcd_test())
             return FC_CONTINUE;
 
-        if (m_params.m_arith_euclidean_solver)
+        if (m_params.m_arith_euclidean_solver || (0 == (1 + m_branch_cut_counter) % 80))
             apply_euclidean_solver();
         
         if (get_context().inconsistent())
diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp
index 13a790e93..f501ed75a 100644
--- a/src/tactic/smtlogics/quant_tactics.cpp
+++ b/src/tactic/smtlogics/quant_tactics.cpp
@@ -22,6 +22,7 @@ Revision History:
 #include"solve_eqs_tactic.h"
 #include"elim_uncnstr_tactic.h"
 #include"qe_tactic.h"
+#include"qe_lite.h"
 #include"qsat.h"
 #include"nlqsat.h"
 #include"ctx_simplify_tactic.h"
@@ -61,6 +62,7 @@ static tactic * mk_no_solve_eq_preprocessor(ast_manager & m) {
 
 tactic * mk_ufnia_tactic(ast_manager & m, params_ref const & p) {
     tactic * st = and_then(mk_no_solve_eq_preprocessor(m),
+                           mk_qe_lite_tactic(m, p),
                            mk_smt_tactic());
     st->updt_params(p);
     return st;