diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 774a76848..f4438a63c 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -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) {
diff --git a/src/test/pdd_solver.cpp b/src/test/pdd_solver.cpp
index 170e887a7..7a1c07131 100644
--- a/src/test/pdd_solver.cpp
+++ b/src/test/pdd_solver.cpp
@@ -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);
             }