diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp
index 14a4e431f..d4eee6832 100644
--- a/src/ast/simplifiers/euf_completion.cpp
+++ b/src/ast/simplifiers/euf_completion.cpp
@@ -66,7 +66,7 @@ namespace euf {
         m_canonical(m),
         m_eargs(m),
         m_canonical_proofs(m),
-        m_infer_patterns(m, m_smt_params),
+        // m_infer_patterns(m, m_smt_params),
         m_deps(m),
         m_rewriter(m) {
         m_tt = m_egraph.mk(m.mk_true(), 0, 0, nullptr);
@@ -241,12 +241,14 @@ namespace euf {
             add_children(n);
             if (is_forall(f)) {
                 quantifier* q = to_quantifier(f);
+#if 0
                 if (q->get_num_patterns() == 0) {
                     expr_ref tmp(m);
                     m_infer_patterns(q, tmp);
                     m_egraph.mk(tmp, 0, 0, nullptr); // ensure tmp is pinned within this scope.
                     q = to_quantifier(tmp);
                 }
+#endif
                 ptr_vector<app> ground;
                 for (unsigned i = 0; i < q->get_num_patterns(); ++i) {
                     auto p = to_app(q->get_pattern(i));
@@ -938,4 +940,4 @@ namespace euf {
             }
         }
     }
-}
\ No newline at end of file
+}
diff --git a/src/ast/simplifiers/euf_completion.h b/src/ast/simplifiers/euf_completion.h
index 58c677f27..5bb704223 100644
--- a/src/ast/simplifiers/euf_completion.h
+++ b/src/ast/simplifiers/euf_completion.h
@@ -26,7 +26,7 @@ Author:
 #include "ast/euf/euf_egraph.h"
 #include "ast/euf/euf_mam.h"
 #include "ast/rewriter/th_rewriter.h"
-#include "ast/pattern/pattern_inference.h"
+// #include "ast/pattern/pattern_inference.h"
 #include "params/smt_params.h"
 
 namespace euf {
@@ -128,7 +128,7 @@ namespace euf {
         enode_vector           m_args, m_reps, m_nodes_to_canonize;
         expr_ref_vector        m_canonical, m_eargs;
         proof_ref_vector       m_canonical_proofs;
-        pattern_inference_rw   m_infer_patterns;
+        //        pattern_inference_rw   m_infer_patterns;
         bindings               m_bindings;
         scoped_ptr<binding>    m_tmp_binding;
         unsigned               m_tmp_binding_capacity = 0;