From 39ca5480d7480ce1462d2d326ef920ce0d0d5973 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 11 Dec 2015 18:18:09 +0000 Subject: [PATCH] ensure that formula is skolemized in the smt solver when using MBQI Reviewed by Nikolaj Signed-off-by: Nuno Lopes --- src/smt/asserted_formulas.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index fa0ec62d4..b66e15cb2 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -259,7 +259,7 @@ void asserted_formulas::reduce() { INVOKE(m_params.m_propagate_booleans, propagate_booleans()); INVOKE(m_params.m_propagate_values, propagate_values()); INVOKE(m_params.m_macro_finder && has_quantifiers(), find_macros()); - INVOKE(m_params.m_nnf_cnf, nnf_cnf()); + INVOKE(m_params.m_nnf_cnf || (m_params.m_mbqi && has_quantifiers()), nnf_cnf()); INVOKE(m_params.m_eliminate_and, eliminate_and()); INVOKE(m_params.m_pull_cheap_ite_trees, pull_cheap_ite_trees()); INVOKE(m_params.m_pull_nested_quantifiers && has_quantifiers(), pull_nested_quantifiers());