diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp
index a9c06e698..58757f6b3 100644
--- a/src/sat/smt/array_model.cpp
+++ b/src/sat/smt/array_model.cpp
@@ -23,7 +23,6 @@ namespace array {
     
     
     void solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) { 
-        std::cout << "add-dep " << mk_bounded_pp(n->get_expr(), m) << "\n";
         if (!a.is_array(n->get_expr())) {
             dep.insert(n, nullptr);
             return;
diff --git a/src/sat/smt/bv_delay_internalize.cpp b/src/sat/smt/bv_delay_internalize.cpp
index 87f198dc5..6bc299063 100644
--- a/src/sat/smt/bv_delay_internalize.cpp
+++ b/src/sat/smt/bv_delay_internalize.cpp
@@ -180,7 +180,6 @@ namespace bv {
                 set_delay_internalize(r, internalize_mode::init_bits_only_i); // do not bit-blast this multiplier.
                 expr_ref eq(m.mk_eq(r, arg_value), m);
                 args[i] = n->get_arg(i);
-                std::cout << eq << "@" << s().scope_lvl() << "\n";
                 add_unit(b_internalize(eq));
             }
             return false;
@@ -299,8 +298,6 @@ namespace bv {
         set_delay_internalize(rhs, internalize_mode::no_delay_i);
         expr_ref eq(m.mk_eq(lhs, rhs), m);
         add_unit(b_internalize(eq));
-        TRACE("bv", tout << "low-bits: " << eq << "\n";);
-        std::cout << "low bits\n";
         return false;     
     }
 
@@ -321,7 +318,10 @@ namespace bv {
     };
 
     /**
+<<<<<<< HEAD
 
+=======
+>>>>>>> 055902df2... bv
      * The i'th bit in xs is 1 if the least significant bit of x is i or lower.
      */
     void solver::encode_lsb_tail(expr* x, expr_ref_vector& xs) {
@@ -388,7 +388,6 @@ namespace bv {
         auto r2 = eval_args(n, args);
         if (r1 == r2)
             return true;
-
         if (m_cheap_axioms)
             return true;
         set_delay_internalize(a, internalize_mode::no_delay_i);
diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp
index eb3cbe10d..d09affb91 100644
--- a/src/sat/smt/bv_solver.cpp
+++ b/src/sat/smt/bv_solver.cpp
@@ -500,7 +500,6 @@ namespace bv {
         svector<std::pair<expr*, internalize_mode>> delay;
         for (auto kv : m_delay_internalize)
             delay.push_back(std::make_pair(kv.m_key, kv.m_value));
-
         flet<bool> _cheap1(m_cheap_axioms, true);
         for (auto kv : delay) 
             if (!check_delay_internalized(kv.first))
diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h
index d55a23b1b..d3deea85d 100644
--- a/src/sat/smt/bv_solver.h
+++ b/src/sat/smt/bv_solver.h
@@ -272,7 +272,6 @@ namespace bv {
         bool check_mul_zero(app* n, expr_ref_vector const& arg_values, expr* value1, expr* value2);
         bool check_mul_one(app* n, expr_ref_vector const& arg_values, expr* value1, expr* value2);
         bool check_mul_low_bits(app* n, expr_ref_vector const& arg_values, expr* value1, expr* value2);
-
         bool check_umul_no_overflow(app* n, expr_ref_vector const& arg_values, expr* value);
         bool check_bv_eval(euf::enode* n);
         bool check_bool_eval(euf::enode* n);