From 45103637adb2871a1557ef77d1608217f9655646 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 29 Sep 2020 14:34:24 -0700 Subject: [PATCH] fix build Signed-off-by: Nikolaj Bjorner --- src/sat/smt/q_mbi.cpp | 2 +- src/util/lim_vector.h | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index 3856b28a1..50662b49d 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -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(body, vars); + body = subst(body, vars); if (is_forall(q)) body = m.mk_not(body); return body; diff --git a/src/util/lim_vector.h b/src/util/lim_vector.h index 24a4a3f0b..1249a9657 100644 --- a/src/util/lim_vector.h +++ b/src/util/lim_vector.h @@ -19,19 +19,19 @@ Author: #include "util/vector.h" template -class lim_svector : public svector { +class lim_svector : public svector { unsigned_vector m_lim; public: lim_svector() {} void push_scope() { - m_lim.push_back(size()); + m_lim.push_back(this->size()); } void pop_scope(unsigned num_scopes) { SASSERT(num_scopes > 0); unsigned old_sz = m_lim.size() - num_scopes; - shrink(m_lim[old_sz]); + this->shrink(m_lim[old_sz]); m_lim.shrink(old_sz); }