diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
index 974b37a00..cb52a9c85 100644
--- a/src/ast/simplifiers/elim_unconstrained.cpp
+++ b/src/ast/simplifiers/elim_unconstrained.cpp
@@ -121,7 +121,7 @@ eliminate:
 elim_unconstrained::elim_unconstrained(ast_manager& m, dependent_expr_state& fmls) :
     dependent_expr_simplifier(m, fmls), m_inverter(m), m_lt(*this), m_heap(1024, m_lt), m_trail(m), m_args(m) {
     std::function<bool(expr*)> is_var = [&](expr* e) {
-        return is_uninterp_const(e) && !m_fmls.frozen(e) && get_node(e).is_root() && get_node(e).num_parents() <= 1;
+        return is_uninterp_const(e) && !m_fmls.frozen(e) && !m_disabled.is_marked(e) && get_node(e).is_root() && get_node(e).num_parents() <= 1;
     };
     m_inverter.set_is_var(is_var);
 }
@@ -247,10 +247,12 @@ elim_unconstrained::node& elim_unconstrained::get_node(expr* t) {
                     m_heap.increased(arg->get_id());
             }
         }
-        else if (is_quantifier(t)) {            
-            node& ch = get_node(to_quantifier(t)->get_expr());
+        else if (is_quantifier(t)) {        
+            auto body = to_quantifier(t)->get_expr();
+            node& ch = get_node(body);
             SASSERT(ch.is_root());
             ch.add_parent(*n);
+            disable(body);
         }
     }
     return *n;
@@ -436,6 +438,7 @@ void elim_unconstrained::reduce() {
         assert_normalized(old_fmls);
         update_model_trail(*mc, old_fmls);
         mc->reset();        
+        m_disabled.reset();
     }
 }
 
@@ -443,3 +446,21 @@ void elim_unconstrained::updt_params(params_ref const& p) {
     smt_params_helper sp(p);
     m_config.m_enabled = sp.elim_unconstrained();
 }
+
+void elim_unconstrained::disable(expr* e) {
+    if (m_disabled.is_marked(e))
+        return;
+
+    ptr_buffer<expr> todo;
+    todo.push_back(e);
+    while (!todo.empty()) {
+        e = todo.back();
+        todo.pop_back();
+        if (m_disabled.is_marked(e))
+            continue;
+        m_disabled.mark(e);
+        if (is_app(e))
+            for (auto arg : *to_app(e))
+                todo.push_back(arg);
+    }
+}
diff --git a/src/ast/simplifiers/elim_unconstrained.h b/src/ast/simplifiers/elim_unconstrained.h
index 4a248b44f..4a946c191 100644
--- a/src/ast/simplifiers/elim_unconstrained.h
+++ b/src/ast/simplifiers/elim_unconstrained.h
@@ -92,6 +92,7 @@ class elim_unconstrained : public dependent_expr_simplifier {
     stats                    m_stats;
     config                   m_config;
     bool                     m_created_compound = false;
+    expr_mark m_disabled;
 
     bool is_var_lt(int v1, int v2) const;
     node& get_node(unsigned n) const { return *m_nodes[n]; }
@@ -108,6 +109,7 @@ class elim_unconstrained : public dependent_expr_simplifier {
     expr* reconstruct_term(node& n);
     void assert_normalized(vector<dependent_expr>& old_fmls);
     void update_model_trail(generic_model_converter& mc, vector<dependent_expr> const& old_fmls);
+    void disable(expr *e);
 
         
 public:
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index 432f0e9e1..9caf76c4a 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -25,6 +25,7 @@ Notes:
 #include "ast/array_decl_plugin.h"
 #include "ast/datatype_decl_plugin.h"
 #include "ast/seq_decl_plugin.h"
+#include "ast/for_each_expr.h"
 #include "tactic/core/collect_occs.h"
 #include "ast/ast_smt2_pp.h"
 #include "ast/ast_ll_pp.h"
@@ -39,7 +40,8 @@ class elim_uncnstr_tactic : public tactic {
     struct rw_cfg : public default_rewriter_cfg {
         bool                   m_produce_proofs;
         obj_hashtable<expr> &  m_vars;
-        obj_hashtable<expr>&   m_nonvars;
+        obj_hashtable<expr>&   m_nonvars;  
+        expr_mark &            m_disabled;
         ref<mc>                m_mc;
         arith_util             m_a_util;
         bv_util                m_bv_util;
@@ -52,11 +54,14 @@ class elim_uncnstr_tactic : public tactic {
         unsigned long long     m_max_memory;
         unsigned               m_max_steps;
         
-        rw_cfg(ast_manager & m, bool produce_proofs, obj_hashtable<expr> & vars, obj_hashtable<expr> & nonvars, mc * _m, 
+        rw_cfg(ast_manager & m, bool produce_proofs, obj_hashtable<expr> & vars, 
+            obj_hashtable<expr> & nonvars, expr_mark& disabled,
+            mc * _m, 
                unsigned long long max_memory, unsigned max_steps):
             m_produce_proofs(produce_proofs),
             m_vars(vars),
-            m_nonvars(nonvars),
+            m_nonvars(nonvars), 
+            m_disabled(disabled),
             m_mc(_m),
             m_a_util(m),
             m_bv_util(m),
@@ -78,7 +83,7 @@ class elim_uncnstr_tactic : public tactic {
         }
         
         bool uncnstr(expr * arg) const {
-            return m_vars.contains(arg) && !m_nonvars.contains(arg);
+            return m_vars.contains(arg) && !m_nonvars.contains(arg) && !m_disabled.is_marked(arg);
         }
         
         bool uncnstr(unsigned num, expr * const * args) const {
@@ -878,10 +883,11 @@ class elim_uncnstr_tactic : public tactic {
     class rw : public rewriter_tpl<rw_cfg> {
         rw_cfg m_cfg;
     public:
-        rw(ast_manager & m, bool produce_proofs, obj_hashtable<expr> & vars, obj_hashtable<expr>& nonvars, mc * _m,
+        rw(ast_manager & m, bool produce_proofs, obj_hashtable<expr> & vars, obj_hashtable<expr>& nonvars, 
+            expr_mark& disabled, mc * _m,
             unsigned long long max_memory, unsigned max_steps):
             rewriter_tpl<rw_cfg>(m, produce_proofs, m_cfg),
-            m_cfg(m, produce_proofs, vars, nonvars, _m, max_memory, max_steps) {
+            m_cfg(m, produce_proofs, vars, nonvars, disabled, _m, max_memory, max_steps) {
         }
     };
     
@@ -889,6 +895,8 @@ class elim_uncnstr_tactic : public tactic {
     ref<mc>                          m_mc;
     obj_hashtable<expr>              m_vars;
     obj_hashtable<expr>              m_nonvars;
+    expr_mark                        m_disabled;
+    expr_ref_vector                  m_pinned;
     scoped_ptr<rw>                   m_rw;
     unsigned                         m_num_elim_apps = 0;
     unsigned long long               m_max_memory;
@@ -903,7 +911,7 @@ class elim_uncnstr_tactic : public tactic {
     }
     
     void init_rw(bool produce_proofs) {
-        m_rw = alloc(rw, m(), produce_proofs, m_vars, m_nonvars, m_mc.get(), m_max_memory, m_max_steps);            
+        m_rw = alloc(rw, m(), produce_proofs, m_vars, m_nonvars, m_disabled, m_mc.get(), m_max_memory, m_max_steps);            
     }
 
     void run(goal_ref const & g, goal_ref_buffer & result) {
@@ -914,6 +922,7 @@ class elim_uncnstr_tactic : public tactic {
         m_vars.reset();
         collect_occs p;
         p(*g, m_vars);
+        disable_quantified(g);
         if (m_vars.empty() || recfun::util(m()).has_rec_defs()) {
             result.push_back(g.get());
             // did not increase depth since it didn't do anything.
@@ -931,6 +940,7 @@ class elim_uncnstr_tactic : public tactic {
         unsigned round = 0;
         unsigned size  = g->size();
         unsigned idx   = 0;
+
         while (true) {
             for (; idx < size; ++idx) {
                 expr * f = g->form(idx);
@@ -964,6 +974,7 @@ class elim_uncnstr_tactic : public tactic {
             size       = g->size();
             m_rw->reset(); // reset cache
             m_vars.reset(); 
+            disable_quantified(g);
             {
                 collect_occs p;
                 p(*g, m_vars);
@@ -974,11 +985,42 @@ class elim_uncnstr_tactic : public tactic {
                 idx = 0;
         }
     }
+
+    void disable(expr* e) {
+        if (m_disabled.is_marked(e))
+            return;
+        m_pinned.push_back(e);
+
+        ptr_buffer<expr> todo;
+        todo.push_back(e);
+        while (!todo.empty()) {
+            e = todo.back();
+            todo.pop_back();
+            if (m_disabled.is_marked(e))
+                continue;
+            m_disabled.mark(e);
+            if (is_app(e))
+                for (auto arg : *to_app(e))
+                    todo.push_back(arg);
+        }
+    }
+
+    void disable_quantified(goal_ref const &g) {
+        m_disabled.reset();
+        m_pinned.reset();
+
+        for (unsigned idx = 0; idx < g->size(); ++idx) {
+            expr *f = g->form(idx);
+            for (expr *e : subterms::all(expr_ref(f, m())))
+                if (is_quantifier(e))
+                    disable(to_quantifier(e)->get_expr());
+        }
+    }
     
     params_ref m_params;
 public:
    elim_uncnstr_tactic(ast_manager & m, params_ref const & p):
-        m_manager(m), m_params(p) {
+        m_manager(m), m_pinned(m), m_params(p) {
         updt_params(p);
     }