diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp
index 39e648a36..a9c06e698 100644
--- a/src/sat/smt/array_model.cpp
+++ b/src/sat/smt/array_model.cpp
@@ -66,7 +66,6 @@ namespace array {
     
         if (!fi->get_else()) {
             expr* else_value = nullptr;
-
             unsigned max_occ_num = 0;
             obj_map<expr, unsigned> num_occ;
             for (euf::enode* p : euf::enode_parents(n)) {
@@ -84,7 +83,6 @@ namespace array {
                     }
                 }
             }
-
             if (else_value)
                 fi->set_else(else_value);
         }
diff --git a/src/sat/smt/bv_delay_internalize.cpp b/src/sat/smt/bv_delay_internalize.cpp
index 6af9ffcf9..a18bbd2b6 100644
--- a/src/sat/smt/bv_delay_internalize.cpp
+++ b/src/sat/smt/bv_delay_internalize.cpp
@@ -77,6 +77,7 @@ namespace bv {
         if (!check_mul_one(e, args, r1, r2))
             return false;
 
+
         // Add propagation axiom for arguments
         if (!check_mul_invertibility(e, args, r1))
             return false;
@@ -157,6 +158,7 @@ namespace bv {
         return ok;
     }
 
+
     /*
     * Check that multiplication with 0 is correctly propagated.
     * If not, create algebraic axioms enforcing 0*x = 0 and x*0 = 0
@@ -423,9 +425,9 @@ namespace bv {
         internalize_mode mode;
         switch (to_app(e)->get_decl_kind()) {
         case OP_BMUL: 
-        case OP_BSMUL_NO_OVFL:
-        case OP_BSMUL_NO_UDFL:
-        case OP_BUMUL_NO_OVFL:
+        //case OP_BSMUL_NO_OVFL:
+        //case OP_BSMUL_NO_UDFL:
+        //case OP_BUMUL_NO_OVFL:
         case OP_BSMOD_I:
         case OP_BUREM_I:
         case OP_BSREM_I: