diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index e2e01bbee..56a89d346 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -479,15 +479,15 @@ bool compare_nodes(ast const * n1, ast const * n2) {
         return
             q1->get_kind()         == q2->get_kind() &&
             q1->get_num_decls()    == q2->get_num_decls() &&
+            q1->get_expr()         == q2->get_expr() &&
+            q1->get_weight()       == q2->get_weight() &&
+            q1->get_num_patterns() == q2->get_num_patterns() &&
             compare_arrays(q1->get_decl_sorts(),
                            q2->get_decl_sorts(),
                            q1->get_num_decls()) &&
             compare_arrays(q1->get_decl_names(),
                            q2->get_decl_names(),
                            q1->get_num_decls()) &&
-            q1->get_expr()         == q2->get_expr() &&
-            q1->get_weight()       == q2->get_weight() &&
-            q1->get_num_patterns() == q2->get_num_patterns() &&
             ((q1->get_qid().is_numerical() && q2->get_qid().is_numerical()) ||
              (q1->get_qid() == q2->get_qid())) && 
             compare_arrays(q1->get_patterns(),
@@ -542,22 +542,6 @@ inline unsigned ast_array_hash(T * const * array, unsigned size, unsigned init_v
     } }
 }
 
-unsigned get_asts_hash(unsigned sz, ast * const* ns, unsigned init) {
-    return ast_array_hash<ast>(ns, sz, init);
-}
-unsigned get_apps_hash(unsigned sz, app * const* ns, unsigned init) {
-    return ast_array_hash<app>(ns, sz, init);
-}
-unsigned get_exprs_hash(unsigned sz, expr * const* ns, unsigned init) {
-    return ast_array_hash<expr>(ns, sz, init);
-}
-unsigned get_sorts_hash(unsigned sz, sort * const* ns, unsigned init) {
-    return ast_array_hash<sort>(ns, sz, init);
-}
-unsigned get_decl_hash(unsigned sz, func_decl* const* ns, unsigned init) {
-    return ast_array_hash<func_decl>(ns, sz, init);
-}
-
 unsigned get_node_hash(ast const * n) {
     unsigned a, b, c;
 
diff --git a/src/ast/ast.h b/src/ast/ast.h
index d7a715cd1..b4b3b1b2f 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -970,11 +970,6 @@ inline quantifier const * to_quantifier(ast const * n) { SASSERT(is_quantifier(n
 unsigned get_node_hash(ast const * n);
 bool compare_nodes(ast const * n1, ast const * n2);
 unsigned get_node_size(ast const * n);
-unsigned get_asts_hash(unsigned sz, ast * const* ns, unsigned init);
-unsigned get_apps_hash(unsigned sz, app * const* ns, unsigned init);
-unsigned get_exprs_hash(unsigned sz, expr * const* ns, unsigned init);
-unsigned get_sorts_hash(unsigned sz, sort * const* ns, unsigned init);
-unsigned get_decl_hash(unsigned sz, func_decl* const* ns, unsigned init);
 
 // This is the internal comparison functor for hash-consing AST nodes.
 struct ast_eq_proc {
diff --git a/src/qe/mbp/mbp_arrays_tg.cpp b/src/qe/mbp/mbp_arrays_tg.cpp
index 8f127819d..d3ed1a9eb 100644
--- a/src/qe/mbp/mbp_arrays_tg.cpp
+++ b/src/qe/mbp/mbp_arrays_tg.cpp
@@ -278,7 +278,6 @@ struct mbp_array_tg::impl {
         m_tg.get_terms(terms, false);
         for (unsigned i = 0; i < terms.size(); i++) {
             term = terms.get(i);
-            SASSERT(!m.is_distinct(term));
             if (m_seen.is_marked(term)) continue;
             if (m_tg.is_cgr(term)) continue;
             TRACE("mbp_tg", tout << "processing " << expr_ref(term, m););
diff --git a/src/qe/mbp/mbp_basic_tg.cpp b/src/qe/mbp/mbp_basic_tg.cpp
index d85215d17..5eca04151 100644
--- a/src/qe/mbp/mbp_basic_tg.cpp
+++ b/src/qe/mbp/mbp_basic_tg.cpp
@@ -43,32 +43,106 @@ struct mbp_basic_tg::impl {
     void mark_seen(expr *t) { m_seen.mark(t); }
     bool is_seen(expr *t) { return m_seen.is_marked(t); }
 
-    //Split on all ite terms, irrespective of whether
-    //they contain variables/are c-ground
+    // Split on all ite terms, irrespective of whether
+    // they contain variables/are c-ground
     bool apply() {
-        if (!m_use_mdl) return false;
+        std::function<bool(expr *)> should_split, is_true, is_false;
+        if (!m_use_mdl) {
+            should_split = [&](expr *t) { return m_tg.has_val_in_class(t); };
+            is_true = [&](expr *t) {
+                return m_tg.has_val_in_class(t) && m_mdl.is_true(t);
+            };
+            is_false = [&](expr *t) {
+                return m_tg.has_val_in_class(t) && m_mdl.is_false(t);
+            };
+        } else {
+            should_split = [](expr *t) { return true; };
+            is_true = [&](expr *t) { return m_mdl.is_true(t); };
+            is_false = [&](expr *t) { return m_mdl.is_false(t); };
+        }
+
         expr *c, *th, *el;
         expr_ref nterm(m);
         bool progress = false;
         TRACE("mbp_tg", tout << "Iterating over terms of tg";);
         // Not resetting terms because get_terms calls resize on terms
         m_tg.get_terms(terms, false);
-        for (expr* term : terms) {
-            if (is_seen(term))
-                continue;
-            if (m.is_ite(term, c, th, el)) {
+        for (expr *term : terms) {
+            if (is_seen(term)) continue;
+            if (m.is_ite(term, c, th, el) && should_split(c)) {
                 mark_seen(term);
                 progress = true;
                 if (m_mdl.is_true(c)) {
                     m_tg.add_lit(c);
                     m_tg.add_eq(term, th);
-                }
-                else {
+                } else {
                     nterm = mk_not(m, c);
                     m_tg.add_lit(nterm);
                     m_tg.add_eq(term, el);
                 }
             }
+            if (m.is_implies(term, c, th)) {
+                if (is_true(th) || is_false(c)) {
+                    mark_seen(term);
+                    progress = true;
+                    if (is_true(th))
+                        m_tg.add_lit(th);
+                    else if (is_false(c))
+                        m_tg.add_lit(c);
+                    m_tg.add_eq(term, m.mk_true());
+                } else if (is_true(c) && is_false(th)) {
+                    mark_seen(term);
+                    progress = true;
+                    m_tg.add_eq(term, m.mk_false());
+                }
+            }
+            if (m.is_or(term) || m.is_and(term)) {
+                bool is_or = m.is_or(term);
+                app *c = to_app(term);
+                bool t = is_or ? any_of(*c, is_true) : all_of(*c, is_true);
+                bool f = is_or ? all_of(*c, is_false) : all_of(*c, is_false);
+                if (t || f) {
+                    mark_seen(term);
+                    progress = true;
+                    m_tg.add_eq(term, t ? m.mk_true() : m.mk_false());
+                    if (f) {
+                        for (auto a : *c) {
+                            if (is_false(a)) {
+                                m_tg.add_lit(mk_not(m, a));
+                                if (!is_or) break;
+                            }
+                        }
+                    } else {
+                        for (auto a : *c) {
+                            if (is_true(a)) {
+                                m_tg.add_lit(a);
+                                if (is_or) break;
+                            }
+                        }
+                    }
+                }
+            }
+            if (m_use_mdl && m.is_distinct(term)) {
+                mark_seen(term);
+                progress = true;
+                bool eq = false;
+                app *c = to_app(term);
+                for (auto a1 : *c) {
+                    for (auto a2 : *c) {
+                        if (a1 == a2) continue;
+                        if (m_mdl.are_equal(a1, a2)) {
+                            m_tg.add_eq(a1, a2);
+                            eq = true;
+                            break;
+                        } else
+                            m_tg.add_deq(a1, a2);
+                    }
+                }
+                if (eq)
+                    m_tg.add_eq(term, m.mk_false());
+                else
+                    m_tg.add_eq(term, m.mk_true());
+            }
         }
         return progress;
     }
diff --git a/src/qe/mbp/mbp_dt_tg.cpp b/src/qe/mbp/mbp_dt_tg.cpp
index b3b24617d..626e8a0e4 100644
--- a/src/qe/mbp/mbp_dt_tg.cpp
+++ b/src/qe/mbp/mbp_dt_tg.cpp
@@ -158,7 +158,6 @@ struct mbp_dt_tg::impl {
         m_tg.get_terms(terms, false);
         for (unsigned i = 0; i < terms.size(); i++) {
             term = terms.get(i);
-            SASSERT(!m.is_distinct(term));
             if (is_seen(term)) continue;
             if (m_tg.is_cgr(term)) continue;
             if (is_app(term) &&
diff --git a/src/qe/mbp/mbp_qel.cpp b/src/qe/mbp/mbp_qel.cpp
index d50a8c1f6..11b651268 100644
--- a/src/qe/mbp/mbp_qel.cpp
+++ b/src/qe/mbp/mbp_qel.cpp
@@ -178,7 +178,7 @@ class mbp_qel::impl {
 
         std::function<bool(expr *)> non_core = [&](expr *e) {
             if (is_app(e) && is_partial_eq(to_app(e))) return true;
-            if (m.is_ite(e)) return true;
+            if (m.is_ite(e) || m.is_or(e) || m.is_implies(e) || m.is_and(e) || m.is_distinct(e)) return true;
             return red_vars.is_marked(e);
         };
 
diff --git a/src/smt/arith_eq_adapter.cpp b/src/smt/arith_eq_adapter.cpp
index b77a38927..f251d01ae 100644
--- a/src/smt/arith_eq_adapter.cpp
+++ b/src/smt/arith_eq_adapter.cpp
@@ -67,6 +67,8 @@ namespace smt {
             m_ge(ge) {
         }
 
+        ~arith_eq_relevancy_eh() override {}
+
         void operator()(relevancy_propagator & rp) override {
             if (!rp.is_relevant(m_n1))
                 return;
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 7895287ef..64c7bbf2e 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3565,7 +3565,6 @@ namespace smt {
         try {
             internalize_assertions();
         } catch (cancel_exception&) {
-            VERIFY(resource_limits_exceeded());
             return l_undef;
         }
         expr_ref_vector theory_assumptions(m);
@@ -3637,7 +3636,6 @@ namespace smt {
                 TRACE("unsat_core_bug", tout << asms << '\n';);
                 init_assumptions(asms);
             } catch (cancel_exception&) {
-                VERIFY(resource_limits_exceeded());
                 return l_undef;
             }
             TRACE("before_search", display(tout););
@@ -3664,7 +3662,6 @@ namespace smt {
                 for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef;
                 init_assumptions(asms);
             } catch (cancel_exception&) {
-                VERIFY(resource_limits_exceeded());
                 return l_undef;
             }
             for (auto const& clause : clauses) init_clause(clause);
diff --git a/src/smt/smt_relevancy.cpp b/src/smt/smt_relevancy.cpp
index 649d75737..ce6de3ec3 100644
--- a/src/smt/smt_relevancy.cpp
+++ b/src/smt/smt_relevancy.cpp
@@ -123,7 +123,7 @@ namespace smt {
     }
     
     struct relevancy_propagator_imp : public relevancy_propagator {
-        unsigned                       m_qhead;
+        unsigned                       m_qhead = 0;
         expr_ref_vector                m_relevant_exprs; 
         uint_set                       m_is_relevant;
         typedef list<relevancy_eh *>   relevancy_ehs;
@@ -144,14 +144,18 @@ namespace smt {
             unsigned m_trail_lim;
         };
         svector<scope>                 m_scopes;
-        bool                           m_propagating;
+        bool                           m_propagating = false;
 
         relevancy_propagator_imp(context & ctx):
-            relevancy_propagator(ctx), m_qhead(0), m_relevant_exprs(ctx.get_manager()),
-            m_propagating(false) {}
+            relevancy_propagator(ctx), m_relevant_exprs(ctx.get_manager()) {}
 
         ~relevancy_propagator_imp() override {
-            undo_trail(0);
+            ast_manager & m = get_manager();
+            unsigned i = m_trail.size();
+            while (i != 0) {
+                --i;
+                m.dec_ref(m_trail[i].get_node());
+            }
         }
 
         relevancy_ehs * get_handlers(expr * n) {
diff --git a/src/smt/smt_relevancy.h b/src/smt/smt_relevancy.h
index f64b7d059..f6e3c4659 100644
--- a/src/smt/smt_relevancy.h
+++ b/src/smt/smt_relevancy.h
@@ -41,13 +41,14 @@ namespace smt {
         /**
            \brief Fallback for the two previous methods.
         */
-        virtual void operator()(relevancy_propagator & rp) {}
+        virtual void operator()(relevancy_propagator & rp) = 0;
     };
 
     class simple_relevancy_eh : public relevancy_eh {
         expr * m_target;
     public:
         simple_relevancy_eh(expr * t):m_target(t) {}
+        ~simple_relevancy_eh() override {}
         void operator()(relevancy_propagator & rp) override;
     };
     
@@ -60,6 +61,7 @@ namespace smt {
         expr * m_target;
     public:
         pair_relevancy_eh(expr * s1, expr * s2, expr * t):m_source1(s1), m_source2(s2), m_target(t) {}
+        ~pair_relevancy_eh() override {}
         void operator()(relevancy_propagator & rp) override;
     };
 
diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp
index 079c2f62e..345663b6b 100644
--- a/src/smt/theory_array_full.cpp
+++ b/src/smt/theory_array_full.cpp
@@ -546,7 +546,7 @@ namespace smt {
 
         expr_ref def2(m.mk_app(f, args2.size(), args2.data()), m);
         ctx.get_rewriter()(def2);
-        expr* def1 = mk_default(map);
+        expr_ref def1(mk_default(map), m);
         ctx.internalize(def1, false);
         ctx.internalize(def2, false);
         return try_assign_eq(def1, def2);
@@ -561,7 +561,7 @@ namespace smt {
         SASSERT(is_const(cnst));
         TRACE("array", tout << mk_bounded_pp(cnst->get_expr(), m) << "\n";);
         expr* val = cnst->get_arg(0)->get_expr();
-        expr* def = mk_default(cnst->get_expr());
+        expr_ref def(mk_default(cnst->get_expr()), m);
         ctx.internalize(def, false);
         return try_assign_eq(val, def);
     }
@@ -598,7 +598,7 @@ namespace smt {
             return false;
         m_stats.m_num_default_lambda_axiom++;
         expr* e = arr->get_expr();
-        expr* def = mk_default(e);
+        expr_ref def(mk_default(e), m);
         quantifier* lam = m.is_lambda_def(arr->get_decl());
         TRACE("array", tout << mk_pp(lam, m) << "\n" << mk_pp(e, m) << "\n");
         expr_ref_vector args(m);