mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 13:21:22 +00:00
Code Activity

fix #3153

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-05 09:18:03 +01:00
parent 153d0661fe
commit c9c9efebde
1 changed files with 8 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/qe/qe_lite.cpp
View file

@ -2245,7 +2245,7 @@ class qe_lite::impl {
q, q,
q->get_num_patterns(), new_patterns, q->get_num_patterns(), new_patterns,
q->get_num_no_patterns(), new_no_patterns, result); q->get_num_no_patterns(), new_no_patterns, result);
m_imp.m_rewriter(result); m_imp.m_rewriter(result, result, result_pr);
return true; return true;
} }
}; };
@ -2254,7 +2254,7 @@ class qe_lite::impl {
elim_cfg m_cfg; elim_cfg m_cfg;
public: public:
elim_star(impl& i): elim_star(impl& i):
rewriter_tpl<elim_cfg>(i.m, false, m_cfg), rewriter_tpl<elim_cfg>(i.m, i.m.proofs_enabled(), m_cfg),
m_cfg(i) m_cfg(i)
{} {}
}; };
@ -2334,9 +2334,11 @@ public:
} }
void operator()(expr_ref& fml, proof_ref& pr) { void operator()(expr_ref& fml, proof_ref& pr) {
expr_ref tmp(m); if (!m.proofs_enabled()) {
m_elim_star(fml, tmp, pr); expr_ref tmp(m);
fml = std::move(tmp); m_elim_star(fml, tmp, pr);
fml = std::move(tmp);
}
} }
void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml) { void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml) {
@ -2496,7 +2498,7 @@ public:
} }
} }
if (f != new_f) { if (f != new_f) {
TRACE("qe", tout << mk_pp(f, m) << "\n" << new_f << "\n";); TRACE("qe", tout << mk_pp(f, m) << "\n" << new_f << "\n" << new_pr << "\n";);
g->update(i, new_f, new_pr, g->dep(i)); g->update(i, new_f, new_pr, g->dep(i));
} }
} }