diff --git a/src/sat/smt/euf_relevancy.cpp b/src/sat/smt/euf_relevancy.cpp
index 28ac99d9a..d7f7b9012 100644
--- a/src/sat/smt/euf_relevancy.cpp
+++ b/src/sat/smt/euf_relevancy.cpp
@@ -22,6 +22,31 @@ Author:
 
 namespace euf {
 
+    void solver::add_auto_relevant(expr* e) {
+        if (!relevancy_enabled())
+            return;
+        for (; m_auto_relevant_scopes > 0; --m_auto_relevant_scopes) 
+            m_auto_relevant_lim.push_back(m_auto_relevant.size());
+        m_auto_relevant.push_back(e);
+    }
+    
+    void solver::pop_relevant(unsigned n) {
+        if (m_auto_relevant_scopes >= n) {
+            m_auto_relevant_scopes -= n;
+            return;
+        }
+        n -= m_auto_relevant_scopes;
+        m_auto_relevant_scopes = 0;
+        unsigned top = m_auto_relevant_lim.size() - n;
+        unsigned lim = m_auto_relevant_lim[top];
+        m_auto_relevant_lim.shrink(top);
+        m_auto_relevant.shrink(lim);        
+    }
+    
+    void solver::push_relevant() {
+        ++m_auto_relevant_scopes;
+    }
+
     bool solver::is_relevant(expr* e) const { 
         return m_relevant_expr_ids.get(e->get_id(), true); 
     }
@@ -31,11 +56,11 @@ namespace euf {
     }
 
     void solver::ensure_dual_solver() {
-        if (!m_dual_solver) {
-            m_dual_solver = alloc(sat::dual_solver, s().rlimit());
-            for (unsigned i = s().num_user_scopes(); i-- > 0; )
-                m_dual_solver->push();
-        }
+        if (m_dual_solver)
+            return;
+        m_dual_solver = alloc(sat::dual_solver, s().rlimit());
+        for (unsigned i = s().num_user_scopes(); i-- > 0; )
+            m_dual_solver->push();        
     }
 
     /**
@@ -65,8 +90,6 @@ namespace euf {
 
     bool solver::init_relevancy() {
         m_relevant_expr_ids.reset();
-        bool_vector visited;
-        ptr_vector<expr> todo;
         if (!relevancy_enabled())
             return true;
         if (!m_dual_solver)
@@ -77,12 +100,16 @@ namespace euf {
         for (enode* n : m_egraph.nodes())
             max_id = std::max(max_id, n->get_expr_id());
         m_relevant_expr_ids.resize(max_id + 1, false);
+        ptr_vector<expr>& todo = m_relevant_todo;
+        bool_vector& visited = m_relevant_visited;
         auto const& core = m_dual_solver->core();
+        todo.reset();
         for (auto lit : core) {
             expr* e = m_bool_var2expr.get(lit.var(), nullptr);
             if (e)
                 todo.push_back(e);
         }
+        todo.append(m_auto_relevant);
         for (unsigned i = 0; i < todo.size(); ++i) {
             expr* e = todo[i];
             if (visited.get(e->get_id(), false))
@@ -114,6 +141,9 @@ namespace euf {
                 todo.push_back(arg);
         }
 
+        for (auto * e : todo)
+            visited[e->get_id()] = false;
+
         TRACE("euf",
             for (enode* n : m_egraph.nodes())
                 if (is_relevant(n)) 
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 3c1831c87..0bbce0993 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -183,6 +183,7 @@ namespace euf {
     }
 
     void solver::propagate(literal lit, ext_justification_idx idx) {
+        add_auto_relevant(bool_var2expr(lit.var()));
         s().assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), idx));
     }
 
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index 2449335d1..0df07faff 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -99,8 +99,7 @@ namespace euf {
         sat::lookahead*        m_lookahead = nullptr;
         ast_manager*           m_to_m;
         sat::sat_internalizer* m_to_si;
-        scoped_ptr<euf::ackerman>    m_ackerman;
-        scoped_ptr<sat::dual_solver> m_dual_solver;
+        scoped_ptr<euf::ackerman>     m_ackerman;
         user_solver::solver*          m_user_propagator = nullptr;
         th_solver*             m_qsolver = nullptr;
         unsigned               m_generation = 0;
@@ -182,6 +181,8 @@ namespace euf {
 
         // relevancy
         bool_vector m_relevant_expr_ids;
+        bool_vector m_relevant_visited;
+        ptr_vector<expr> m_relevant_todo;
         void ensure_dual_solver();
         bool init_relevancy();
 
@@ -363,6 +364,11 @@ namespace euf {
 
         // relevancy
         bool m_relevancy = true;
+        scoped_ptr<sat::dual_solver>  m_dual_solver;
+        ptr_vector<expr>              m_auto_relevant;
+        unsigned_vector               m_auto_relevant_lim;
+        unsigned                      m_auto_relevant_scopes = 0;
+
         bool relevancy_enabled() const { return m_relevancy && get_config().m_relevancy_lvl > 0; }
         void disable_relevancy(expr* e) { IF_VERBOSE(0, verbose_stream() << "disabling relevancy " << mk_pp(e, m) << "\n"); m_relevancy = false;  }
         void add_root(unsigned n, sat::literal const* lits);
@@ -377,6 +383,9 @@ namespace euf {
         void track_relevancy(sat::bool_var v);
         bool is_relevant(expr* e) const;
         bool is_relevant(enode* n) const;
+        void add_auto_relevant(expr* e);
+        void pop_relevant(unsigned n);
+        void push_relevant();
 
 
         // model construction
diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index c0288e5cf..e4e01b964 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -54,7 +54,11 @@ namespace q {
         m_eval(ctx),
         m_qstat_gen(m, ctx.get_region()),
         m_inst_queue(*this, ctx),
-        m_infer_patterns(m, ctx.get_config())       
+        m_infer_patterns(m, ctx.get_config()),
+        m_new_defs(m),
+        m_new_proofs(m),
+        m_dn(m),
+        m_nnf(m, m_dn)
     {
         std::function<void(euf::enode*, euf::enode*)> _on_merge = 
             [&](euf::enode* root, euf::enode* other) { 
@@ -105,6 +109,20 @@ namespace q {
         m_eval.explain(l, justification::from_index(idx), r, probing);
     }
 
+    quantifier_ref ematch::nnf_skolem(quantifier* q) {
+        expr_ref r(m);
+        proof_ref p(m);
+        m_new_defs.reset();
+        m_new_proofs.reset();
+        m_nnf(q, m_new_defs, m_new_proofs, r, p);
+        SASSERT(is_quantifier(r));
+        for (expr* d : m_new_defs)
+            m_qs.add_unit(m_qs.mk_literal(d));
+        CTRACE("q", r != q, tout << mk_pp(q, m) << " -->\n" << r << "\n" << m_new_defs << "\n";);
+        return quantifier_ref(to_quantifier(r), m);
+    }
+
+
     std::ostream& ematch::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const {
         auto& j = justification::from_index(idx);
         auto& c = j.m_clause;
@@ -218,8 +236,6 @@ namespace q {
         }
     };
 
-
-
     binding* ematch::tmp_binding(clause& c, app* pat, euf::enode* const* b) {
         if (c.num_decls() > m_tmp_binding_capacity) {
             void* mem = memory::allocate(sizeof(binding) + c.num_decls() * sizeof(euf::enode*));
@@ -430,7 +446,10 @@ namespace q {
             cl->m_literal.neg();
             expr_ref body(mk_not(m, q->get_expr()), m);
             q = m.update_quantifier(q, forall_k, body);
-        }        
+        }
+        q = nnf_skolem(q);
+        
+        
         expr_ref_vector ors(m);
         flatten_or(q->get_expr(), ors);
         for (expr* arg : ors) 
diff --git a/src/sat/smt/q_ematch.h b/src/sat/smt/q_ematch.h
index 58037e308..3cdcfc80e 100644
--- a/src/sat/smt/q_ematch.h
+++ b/src/sat/smt/q_ematch.h
@@ -19,6 +19,7 @@ Author:
 #include "util/nat_set.h"
 #include "ast/quantifier_stat.h"
 #include "ast/pattern/pattern_inference.h"
+#include "ast/normal_forms/nnf.h"
 #include "solver/solver.h"
 #include "sat/smt/sat_th.h"
 #include "sat/smt/q_mam.h"
@@ -119,6 +120,13 @@ namespace q {
 
         bool propagate(bool flush);
 
+        expr_ref_vector m_new_defs;
+        proof_ref_vector m_new_proofs;
+        defined_names    m_dn;
+        nnf              m_nnf;
+        
+        quantifier_ref nnf_skolem(quantifier* q);
+
     public:
         
         ematch(euf::solver& ctx, solver& s);