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

fixed recently introduced bug

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-11-28 16:46:19 -08:00
parent 830f6ada93
commit 3ca41c6202
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/smt/asserted_formulas.cpp
View file

@ -287,6 +287,7 @@ void asserted_formulas::reduce() {
INVOKE(m_params.m_quasi_macros && has_quantifiers(), apply_quasi_macros()); INVOKE(m_params.m_quasi_macros && has_quantifiers(), apply_quasi_macros());
INVOKE(m_params.m_simplify_bit2int, apply_bit2int()); INVOKE(m_params.m_simplify_bit2int, apply_bit2int());
INVOKE(m_params.m_eliminate_bounds && has_quantifiers(), cheap_quant_fourier_motzkin()); INVOKE(m_params.m_eliminate_bounds && has_quantifiers(), cheap_quant_fourier_motzkin());
INVOKE(m_params.m_ematching && has_quantifiers(), infer_patterns());
INVOKE(m_params.m_max_bv_sharing && has_bv(), max_bv_sharing()); INVOKE(m_params.m_max_bv_sharing && has_bv(), max_bv_sharing());
INVOKE(m_params.m_bb_quantifiers, elim_bvs_from_quantifiers()); INVOKE(m_params.m_bb_quantifiers, elim_bvs_from_quantifiers());
// temporary HACK: make sure that arith & bv are list-assoc // temporary HACK: make sure that arith & bv are list-assoc