mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

fix build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-09-29 14:34:24 -07:00
parent 7787bd399e
commit 45103637ad
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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(body, vars); 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;

6
src/util/lim_vector.h
View file

@ -19,19 +19,19 @@ Author:
#include "util/vector.h" #include "util/vector.h"
template<typename T> template<typename T>
class lim_svector : public svector<T> { class lim_svector : public svector<T, unsigned> {
unsigned_vector m_lim; unsigned_vector m_lim;
public: public:
lim_svector() {} lim_svector() {}
void push_scope() { void push_scope() {
m_lim.push_back(size()); m_lim.push_back(this->size());
} }
void pop_scope(unsigned num_scopes) { void pop_scope(unsigned num_scopes) {
SASSERT(num_scopes > 0); SASSERT(num_scopes > 0);
unsigned old_sz = m_lim.size() - num_scopes; unsigned old_sz = m_lim.size() - num_scopes;
shrink(m_lim[old_sz]); this->shrink(m_lim[old_sz]);
m_lim.shrink(old_sz); m_lim.shrink(old_sz);
} }