mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix #3464

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-22 14:28:56 -07:00
parent 70a1786061
commit 9366311844
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/tactic/arith/purify_arith_tactic.cpp
View file

@ -271,6 +271,7 @@ struct purify_arith_proc {
void push_cnstr(expr * cnstr) {
m_new_cnstrs.push_back(cnstr);
TRACE("purify_arith", tout << mk_pp(cnstr, m()) << "\n";);
}
void cache_result(app * t, expr * r, proof * pr) {
@ -723,20 +724,19 @@ struct purify_arith_proc {
proof_ref new_body_pr(m());
r(q->get_expr(), new_body, new_body_pr);
unsigned num_vars = r.cfg().m_new_vars.size();
expr_ref_vector & cnstrs = r.cfg().m_new_cnstrs;
cnstrs.push_back(new_body);
new_body = m().mk_and(cnstrs.size(), cnstrs.c_ptr());
TRACE("purify_arith",
tout << "num_vars: " << num_vars << "\n";
tout << "body: " << mk_ismt2_pp(q->get_expr(), m()) << "\nnew_body: " << mk_ismt2_pp(new_body, m()) << "\n";);
if (num_vars == 0) {
SASSERT(r.cfg().m_new_cnstrs.empty());
result = m().update_quantifier(q, new_body);
if (m_produce_proofs)
result_pr = m().mk_quant_intro(q, to_quantifier(result.get()), result_pr);
}
else {
// Add new constraints
expr_ref_vector & cnstrs = r.cfg().m_new_cnstrs;
cnstrs.push_back(new_body);
new_body = m().mk_and(cnstrs.size(), cnstrs.c_ptr());
// Open space for new variables
var_shifter shifter(m());
shifter(new_body, num_vars, new_body);