diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 58aa01845..2a56168f2 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -481,7 +481,7 @@ namespace smt { if (!m_fparams->m_ematching) { return; } - if (m_context->get_manager().is_rec_fun_def(q) && mbqi_enabled(q)) { + if (false && m_context->get_manager().is_rec_fun_def(q) && mbqi_enabled(q)) { return; } bool has_unary_pattern = false;