diff --git a/src/ast/euf/euf_bv_plugin.cpp b/src/ast/euf/euf_bv_plugin.cpp
index e9da7065e..3ae04231a 100644
--- a/src/ast/euf/euf_bv_plugin.cpp
+++ b/src/ast/euf/euf_bv_plugin.cpp
@@ -171,7 +171,7 @@ namespace euf {
 
             if (is_extract(p, lo, hi)) {
                 auto val_p = mod2k(machine_div2k(val_x, lo), hi - lo + 1);
-                push_merge(p, mk_value(val_p, width(p)));
+                push_merge(bv.mk_extract(x->get_interpreted(), lo, hi), mk_value(val_p, width(p)));
             }
         }
         
diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp
index e2933aaaa..af2830b92 100644
--- a/src/sat/smt/polysat/viable.cpp
+++ b/src/sat/smt/polysat/viable.cpp
@@ -804,7 +804,7 @@ namespace polysat {
                     return find_t::multiple;
                 }
                 else {
-                    IF_VERBOSE(0, display_one(verbose_stream() << "full: ", v, ne) << "\n");
+                    // IF_VERBOSE(0, display_one(verbose_stream() << "full: ", v, ne) << "\n");
                     SASSERT(hi < lo);
                     ne->interval = eval_interval::full();
                     ne->coeff = 1;
diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp
index 387b5c74f..fa3860d3f 100644
--- a/src/sat/smt/polysat_internalize.cpp
+++ b/src/sat/smt/polysat_internalize.cpp
@@ -515,7 +515,6 @@ namespace polysat {
         pdd b = expr2pdd(y);
         auto& m = a.manager();
         unsigned sz = m.power_of_2();
-        verbose_stream() << "quot-rem " << a << " " << b << "\n";
         if (b.is_zero()) {
             // By SMT-LIB specification, b = 0 ==> q = -1, r = a.
             internalize_set(quot, m.mk_val(m.max_value()));