From 7787bd399e2e7e63f1d5bbf6c1ce96424acc3b81 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 29 Sep 2020 13:53:35 -0700 Subject: [PATCH] nit --- src/sat/smt/q_mbi.cpp | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index a455d3966..3856b28a1 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -105,9 +105,9 @@ namespace q { } expr_ref mbqi::specialize(quantifier* q, expr_ref_vector& vars) { - expr_ref tmp(m); + expr_ref body(m); 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); vars.resize(sz, nullptr); for (unsigned i = 0; i < sz; ++i) { @@ -117,7 +117,7 @@ namespace q { restrict_to_universe(vars.get(i), m_model->get_universe(s)); } var_subst subst(m); - expr_ref body = subst(tmp, vars.size(), vars.c_ptr()); + expr_ref body = subst(body, vars); if (is_forall(q)) body = m.mk_not(body); return body; @@ -156,8 +156,7 @@ namespace q { #endif } var_subst subst(m); - expr_ref body = subst(q->get_expr(), vals.size(), vals.c_ptr()); - return body; + return subst(q->get_expr(), vals); }