mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

re-enable ematching on recursive function definitions, disabling ematching breaks regressions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-11-20 06:24:47 -08:00
parent 650a719298
commit 725e79e9eb
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_quantifier.cpp
View file

@ -481,7 +481,7 @@ namespace smt {
if (!m_fparams->m_ematching) { if (!m_fparams->m_ematching) {
return; 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; return;
} }
bool has_unary_pattern = false; bool has_unary_pattern = false;