diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp
index 2f0d3868c..50a221e4c 100644
--- a/src/ast/simplifiers/euf_completion.cpp
+++ b/src/ast/simplifiers/euf_completion.cpp
@@ -149,8 +149,10 @@ namespace euf {
         for (unsigned i = 0; i < q->get_num_decls(); ++i)
             _binding.push_back(binding[i]->get_expr());
         expr_ref r = subst(q->get_expr(), _binding);
+        IF_VERBOSE(12, verbose_stream() << "add " << r << "\n");
         add_constraint(r, get_dependency(q));
         m_should_propagate = true;
+        ++m_stats.m_num_instances;
     }
 
     void completion::read_egraph() {
@@ -164,8 +166,7 @@ namespace euf {
 
         unsigned sz = qtail();
         for (unsigned i = qhead(); i < sz; ++i) {
-            auto [f, p, d] = m_fmls[i]();
-            
+            auto [f, p, d] = m_fmls[i]();            
             expr_dependency_ref dep(d, m);
             expr_ref g = canonize_fml(f, dep);
             if (g != f) {
@@ -388,6 +389,53 @@ namespace euf {
 
     void completion::collect_statistics(statistics& st) const {
         st.update("euf-completion-rewrites", m_stats.m_num_rewrites);        
+        st.update("euf-completion-instances", m_stats.m_num_instances);        
+    }
+
+    bool completion::is_gt(expr* lhs, expr* rhs) const {
+        if (lhs == rhs) 
+            return false;
+        // values are always less in ordering than non-values.
+        bool v1 = m.is_value(lhs);
+        bool v2 = m.is_value(rhs);
+        if (!v1 && v2) 
+            return true;
+        if (v1 && !v2) 
+            return false;
+        
+        if (get_depth(lhs) > get_depth(rhs)) 
+            return true;
+        if (get_depth(lhs) < get_depth(rhs)) 
+            return false;
+
+        // slow path
+        auto n1 = get_num_exprs(lhs);
+        auto n2 = get_num_exprs(rhs);
+        if (n1 > n2)
+            return true;
+        if (n1 < n2)
+            return false;
+        
+        if (is_app(lhs) && is_app(rhs)) {
+            app* l = to_app(lhs);
+            app* r = to_app(rhs);
+            if (l->get_decl()->get_id() != r->get_decl()->get_id()) 
+                return l->get_decl()->get_id() > r->get_decl()->get_id();
+            if (l->get_num_args() != r->get_num_args()) 
+                return l->get_num_args() > r->get_num_args();
+            for (unsigned i = 0; i < l->get_num_args(); ++i) 
+                if (l->get_arg(i) != r->get_arg(i)) 
+                    return is_gt(l->get_arg(i), r->get_arg(i));
+            UNREACHABLE();
+        }
+        if (is_quantifier(lhs) && is_quantifier(rhs)) {
+            expr* l = to_quantifier(lhs)->get_expr();
+            expr* r = to_quantifier(rhs)->get_expr();
+            return is_gt(l, r);
+        }
+        if (is_quantifier(lhs))
+            return true;
+        return false;
     }
 
     void completion::map_canonical() {
@@ -403,8 +451,9 @@ namespace euf {
             roots.push_back(n);
             enode* rep = nullptr;
             for (enode* k : enode_class(n)) 
-                if (!rep || m.is_value(k->get_expr()) || get_depth(rep->get_expr()) > get_depth(k->get_expr()))
-                    rep = k;
+                if (!rep || m.is_value(k->get_expr()) || is_gt(rep->get_expr(), k->get_expr()))
+                    rep = k;            
+            // IF_VERBOSE(0, verbose_stream() << m_egraph.bpp(n) << " ->\n" << m_egraph.bpp(rep) << "\n";);
             m_reps.setx(n->get_id(), rep, nullptr);
 
             TRACE(euf_completion, tout << "rep " << m_egraph.bpp(n) << " -> " << m_egraph.bpp(rep) << "\n";
diff --git a/src/ast/simplifiers/euf_completion.h b/src/ast/simplifiers/euf_completion.h
index 29d3b709a..4f07578ef 100644
--- a/src/ast/simplifiers/euf_completion.h
+++ b/src/ast/simplifiers/euf_completion.h
@@ -28,6 +28,7 @@ namespace euf {
 
         struct stats {
             unsigned m_num_rewrites = 0;
+            unsigned m_num_instances = 0;
             void reset() { memset(this, 0, sizeof(*this)); }
         };
 
@@ -63,6 +64,8 @@ namespace euf {
         expr_dependency* explain_eq(enode* a, enode* b);
         expr_dependency* explain_conflict();
         expr_dependency* get_dependency(quantifier* q) { return m_q2dep.contains(q) ? m_q2dep[q] : nullptr; }
+
+        bool is_gt(expr* a, expr* b) const;
     public:
         completion(ast_manager& m, dependent_expr_state& fmls);
         char const* name() const override { return "euf-reduce"; }
diff --git a/src/ast/simplifiers/extract_eqs.cpp b/src/ast/simplifiers/extract_eqs.cpp
index 470bec88d..cc9854687 100644
--- a/src/ast/simplifiers/extract_eqs.cpp
+++ b/src/ast/simplifiers/extract_eqs.cpp
@@ -33,6 +33,40 @@ namespace euf {
         bool m_ite_solver = true;
         bool m_allow_bool = true;
 
+        bool is_eq_of(expr* x, expr* y, expr*& z, expr*& s, expr*& t) {
+            expr* x1 = nullptr, *x2 = nullptr, *y1 = nullptr, *y2 = nullptr;
+            if (!m.is_eq(x, x1, x2))
+                return false;
+            if (!m.is_eq(y, y1, y2))
+                return false;
+            if (x1 == y1) {
+                z = x1;
+                s = x2;
+                t = y2;
+                return true;
+            }
+            if (x1 == y2) {
+                z = x1;
+                s = x2;
+                t = y1;
+                return true;
+            }
+            if (x2 == y1) {
+                z = x2;
+                s = x1;
+                t = y2;
+                return true;
+            }
+            return false;
+        }
+        bool is_complementary(expr* x, expr* y) {
+            expr* z = nullptr;
+            if (m.is_not(x, z) && z == y)
+                return true;
+            if (m.is_not(y, z) && z == x)
+                return true;
+            return false;
+        }
     public:
         basic_extract_eq(ast_manager& m) : m(m) {}
 
@@ -68,6 +102,30 @@ namespace euf {
                         eqs.push_back(dependent_eq(e.fml(), to_app(x1), expr_ref(m.mk_ite(c, y1, y2), m), d));
                 }
             }
+            // (or (and a (= x t)) (and (not a) (= x s)))
+            // -> x = if a s t
+            if (m.is_or(f, x1, y1) && m.is_and(x1, x1, x2) && m.is_and(y1, y1, y2)) {
+                expr* z = nullptr, *t = nullptr, *s = nullptr;
+                if (is_eq_of(x1, y1, z, s, t) && is_complementary(x2, y2)) 
+                    eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(x2, s, t), m), d));
+                if (is_eq_of(x1, y2, z, s, t) && is_complementary(x2, y1))
+                    eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(x2, s, t), m), d));
+                if (is_eq_of(x2, y2, z, s, t) && is_complementary(x1, y1))
+                    eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(x1, s, t), m), d));
+                if (is_eq_of(x2, y1, z, s, t) && is_complementary(x1, y2))
+                    eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(x1, s, t), m), d));
+            }
+            if (m.is_and(f, x1, y1) && m.is_or(x, x1, x2) && m.is_or(y1, y1, y2)) {
+                expr* z = nullptr, *t = nullptr, *s = nullptr;
+                if (is_eq_of(x1, y1, z, s, t) && is_complementary(x2, y2)) 
+                    eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(y2, s, t), m), d));
+                if (is_eq_of(x1, y2, z, s, t) && is_complementary(x2, y1))
+                    eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(y1, s, t), m), d));
+                if (is_eq_of(x2, y2, z, s, t) && is_complementary(x1, y1))
+                    eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(y1, s, t), m), d));
+                if (is_eq_of(x2, y1, z, s, t) && is_complementary(x1, y2))
+                    eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(y2, s, t), m), d));
+            }
             if (!m_allow_bool)
                 return;
             if (is_uninterp_const(f))
diff --git a/src/math/grobner/pdd_solver.cpp b/src/math/grobner/pdd_solver.cpp
index 1d57a673d..4afd27704 100644
--- a/src/math/grobner/pdd_solver.cpp
+++ b/src/math/grobner/pdd_solver.cpp
@@ -72,7 +72,7 @@ namespace dd {
 
     void solver::adjust_cfg() {
         auto & cfg = m_config;
-        IF_VERBOSE(3, verbose_stream() << "start saturate\n"; display_statistics(verbose_stream()));
+        IF_VERBOSE(5, verbose_stream() << "start saturate\n"; display_statistics(verbose_stream()));
         cfg.m_eqs_threshold = static_cast<unsigned>(cfg.m_eqs_growth * ceil(log(1 + m_to_simplify.size()))* m_to_simplify.size());
         cfg.m_expr_size_limit = 0;
         cfg.m_expr_degree_limit = 0;
@@ -83,7 +83,7 @@ namespace dd {
         cfg.m_expr_size_limit *= cfg.m_expr_size_growth;
         cfg.m_expr_degree_limit *= cfg.m_expr_degree_growth;;
         
-        IF_VERBOSE(3, verbose_stream() << "set m_config.m_eqs_threshold " <<  m_config.m_eqs_threshold  << "\n";
+        IF_VERBOSE(5, verbose_stream() << "set m_config.m_eqs_threshold " <<  m_config.m_eqs_threshold  << "\n";
                    verbose_stream() << "set m_config.m_expr_size_limit to " <<  m_config.m_expr_size_limit << "\n";
                    verbose_stream() << "set m_config.m_expr_degree_limit to " <<  m_config.m_expr_degree_limit << "\n";
                    );
@@ -98,7 +98,7 @@ namespace dd {
             while (!done() && step()) {
                 TRACE(dd_solver, display(tout););
                 DEBUG_CODE(invariant(););
-                IF_VERBOSE(3, display_statistics(verbose_stream()));
+                IF_VERBOSE(6, display_statistics(verbose_stream()));
             }
             DEBUG_CODE(invariant(););
         }
diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 6cf57c551..9f5abb51a 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -86,8 +86,8 @@ namespace nla {
         if (m_quota > 0)
            --m_quota;
 
-        IF_VERBOSE(3, verbose_stream() << "grobner miss, quota " << m_quota << "\n");
-        IF_VERBOSE(4, diagnose_pdd_miss(verbose_stream()));
+        IF_VERBOSE(5, verbose_stream() << "grobner miss, quota " << m_quota << "\n");
+        IF_VERBOSE(5, diagnose_pdd_miss(verbose_stream()));
     }
 
     dd::solver::equation_vector const& grobner::core_equations(bool all_eqs) {
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 1e4414afe..fd71ac433 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3789,19 +3789,19 @@ public:
     unsigned m_num_dumped_lemmas = 0;
 
     void dump_assign_lemma(literal lit) {
-        std::cout << "; assign lemma " << (m_num_dumped_lemmas++) << "\n";
+        std::cout << "(echo \"assign lemma " << (m_num_dumped_lemmas++) << "\")\n";
         ctx().display_lemma_as_smt_problem(std::cout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), lit);
         std::cout << "(reset)\n";
     }
 
     void dump_conflict() {
-        std::cout << "; conflict " << (m_num_dumped_lemmas++) << "\n";
+        std::cout << "(echo \"conflict " << (m_num_dumped_lemmas++) << "\")\n";
         ctx().display_lemma_as_smt_problem(std::cout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data());
         std::cout << "(reset)\n";
     }
 
     void dump_eq(enode* x, enode* y) {
-        std::cout << "; equality propagation " << (m_num_dumped_lemmas++) << "\n";
+        std::cout << "(echo \"equality propagation " << (m_num_dumped_lemmas++) << "\")\n";
         ctx().display_lemma_as_smt_problem(std::cout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), false_literal, symbol::null, x, y);
         std::cout << "(reset)\n";
     }