mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fix build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-20 11:19:26 -07:00
parent 6f31d83633
commit fd799089b7
2 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -868,7 +868,7 @@ namespace euf {
if (b != sat::null_bool_var) {
m_bool_var2expr.setx(b, n->get_expr(), nullptr);
SASSERT(r->m.is_bool(n->get_sort()));
IF_VERBOSE(0, verbose_stream() << "set bool_var " << r->bpp(n) << "\n");
IF_VERBOSE(1, verbose_stream() << "set bool_var " << r->bpp(n) << "\n");
}
}
for (auto* s_orig : m_id2solver) {

6
src/test/pdd_solver.cpp
View file

@ -182,7 +182,7 @@ namespace dd {
void collect_id2var(unsigned_vector& id2var, expr_ref_vector const& fmls) {
svector<std::pair<unsigned, unsigned>> ds;
unsigned maxid = 0;
for (expr* e : subterms(fmls)) {
for (expr* e : subterms::ground(fmls)) {
ds.push_back(std::make_pair(to_app(e)->get_depth(), e->get_id()));
maxid = std::max(maxid, e->get_id());
}
@ -202,11 +202,11 @@ namespace dd {
pdd_manager p(id2var.size(), use_mod2 ? pdd_manager::mod2_e : pdd_manager::zero_one_vars_e);
solver g(m.limit(), p);
for (expr* e : subterms(fmls)) {
for (expr* e : subterms::ground(fmls)) {
add_def(id2var, to_app(e), m, p, g);
}
if (!use_mod2) { // should be built-in
for (expr* e : subterms(fmls)) {
for (expr* e : subterms::ground(fmls)) {
pdd v = p.mk_var(id2var[e->get_id()]);
g.add(v*v - v);
}