mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

Added bv_sort_ac=true to asserted_formulas::m_rewriter

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-10-09 19:18:41 +01:00
parent 5819e38606
commit 800fa3d246
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/asserted_formulas.cpp
View file

@ -130,6 +130,7 @@ void asserted_formulas::set_eliminate_and(bool flag) {
p.set_bool("eq2ineq", m_params.m_arith_eq2ineq); p.set_bool("eq2ineq", m_params.m_arith_eq2ineq);
p.set_bool("gcd_rounding", true); p.set_bool("gcd_rounding", true);
p.set_bool("expand_select_store", true); p.set_bool("expand_select_store", true);
p.set_bool("bv_sort_ac", true);
m_rewriter.updt_params(p); m_rewriter.updt_params(p);
flush_cache(); flush_cache();
} }
@ -142,8 +143,6 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
if (inconsistent()) if (inconsistent())
return; return;
m_has_quantifiers |= ::has_quantifiers(e);
if (m_params.m_preprocess) { if (m_params.m_preprocess) {
TRACE("assert_expr_bug", tout << r << "\n";); TRACE("assert_expr_bug", tout << r << "\n";);
set_eliminate_and(false); // do not eliminate and before nnf. set_eliminate_and(false); // do not eliminate and before nnf.
@ -156,6 +155,9 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
} }
TRACE("assert_expr_bug", tout << "after...\n" << r << "\n";); TRACE("assert_expr_bug", tout << "after...\n" << r << "\n";);
} }
m_has_quantifiers |= ::has_quantifiers(e);
push_assertion(r, pr, m_formulas); push_assertion(r, pr, m_formulas);
TRACE("asserted_formulas_bug", tout << "after assert_expr\n"; display(tout);); TRACE("asserted_formulas_bug", tout << "after assert_expr\n"; display(tout););
} }