From 725e79e9eb5fdb6d321ad7763ed3f8f8c5f13f48 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 20 Nov 2016 06:24:47 -0800
Subject: [PATCH] re-enable ematching on recursive function definitions,
 disabling ematching breaks regressions

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_quantifier.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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;