mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

ensure that formula is skolemized in the smt solver when using MBQI

Browse source 
Reviewed by Nikolaj

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2015-12-11 18:18:09 +00:00
parent ef06da8c2c
commit 39ca5480d7
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/asserted_formulas.cpp
View file

@ -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());