mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 11:20:26 +00:00
Code Activity

fix push/pop bug for ite-elimination, thanks to Nao Hirokawa for reporting it

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-08-30 08:31:37 -03:00
parent de43e05102
commit 4c0db00a7b
4 changed files with 13 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/asserted_formulas.h
View file

@ -156,6 +156,8 @@ class asserted_formulas {
void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_elim(j.get_fml(), n, p); }
bool should_apply() const override { return af.m_smt_params.m_eliminate_term_ite && af.m_smt_params.m_lift_ite != LI_FULL; }
void post_op() override { af.m_formulas.append(m_elim.new_defs()); af.reduce_and_solve(); m_elim.reset(); }
void push() { m_elim.push(); }
void pop(unsigned n) { m_elim.pop(n); }
};
#define MK_SIMPLIFIERA(NAME, FUNCTOR, MSG, APP, ARG, REDUCE) \