diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
index 9354b53f6c0..a92799c4c71 100644
--- a/src/ast/rewriter/bool_rewriter.cpp
+++ b/src/ast/rewriter/bool_rewriter.cpp
@@ -282,7 +282,7 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args
                 get_num_internal_exprs(m_counts2, m_todo2, args[i]);
             unsigned count1 = count_internal_nodes(m_counts1, m_todo1);
             unsigned count2 = count_internal_nodes(m_counts2, m_todo2);
-            if (count1 > count2)
+            if (count1 > count2 + num_args)
                 st = BR_FAILED;
         }
         if (st != BR_FAILED)
diff --git a/src/ast/rewriter/hoist_rewriter.cpp b/src/ast/rewriter/hoist_rewriter.cpp
index 72a764bfa37..7b217fc2421 100644
--- a/src/ast/rewriter/hoist_rewriter.cpp
+++ b/src/ast/rewriter/hoist_rewriter.cpp
@@ -137,11 +137,17 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref &
             m_subst.insert(p, m.mk_true());
         fmls.push_back(p);
     }
-    for (auto& p : m_eqs) {
-        if (m.is_value(p.first))
-            std::swap(p.first, p.second);
-        m_subst.insert(p.first, p.second);
-        fmls.push_back(m.mk_eq(p.first, p.second));
+    for (auto& [a, b] : m_eqs) {
+        if (m.is_value(a))
+            std::swap(a, b);
+        if (m.are_equal(a, b))
+            continue;
+        if (m.are_distinct(a, b)) {
+            result = m.mk_false();
+            return BR_DONE;
+        }
+        m_subst.insert(a, b);
+        fmls.push_back(m.mk_eq(a, b));        
     }    
     expr_ref ors(::mk_or(m, num_args, es), m);
     m_subst(ors);
diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index 3804b72284e..b9ac45039f2 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -2413,7 +2413,10 @@ namespace {
             m_n2 = static_cast<const check *>(m_pc)->m_enode;
             SASSERT(m_n1 != 0);
             SASSERT(m_n2 != 0);
-            if (m_n1->get_root() != m_n2->get_root())
+
+            // hack to handle dynamically generated patterns:
+            // if the pattern is ground and an if-expression, ignore equality check.
+            if (m_n1->get_root() != m_n2->get_root() && !m.is_ite(m_n2->get_expr()))
                 goto backtrack;
 
             // we used the equality m_n1 = m_n2 for the match and need to make sure it ends up in the log