mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

nit

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-09-29 13:53:35 -07:00
parent 5df2715064
commit 7787bd399e
1 changed files with 4 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/sat/smt/q_mbi.cpp
View file

@ -105,9 +105,9 @@ namespace q {
} }
expr_ref mbqi::specialize(quantifier* q, expr_ref_vector& vars) { expr_ref mbqi::specialize(quantifier* q, expr_ref_vector& vars) {
expr_ref tmp(m); expr_ref body(m);
unsigned sz = q->get_num_decls(); unsigned sz = q->get_num_decls();
if (!m_model->eval_expr(q->get_expr(), tmp, true)) if (!m_model->eval_expr(q->get_expr(), body, true))
return expr_ref(m); return expr_ref(m);
vars.resize(sz, nullptr); vars.resize(sz, nullptr);
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
@ -117,7 +117,7 @@ namespace q {
restrict_to_universe(vars.get(i), m_model->get_universe(s)); restrict_to_universe(vars.get(i), m_model->get_universe(s));
} }
var_subst subst(m); var_subst subst(m);
expr_ref body = subst(tmp, vars.size(), vars.c_ptr()); expr_ref body = subst(body, vars);
if (is_forall(q)) if (is_forall(q))
body = m.mk_not(body); body = m.mk_not(body);
return body; return body;
@ -156,8 +156,7 @@ namespace q {
#endif #endif
} }
var_subst subst(m); var_subst subst(m);
expr_ref body = subst(q->get_expr(), vals.size(), vals.c_ptr()); return subst(q->get_expr(), vals);
return body;
} }