diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index efdf8a39a..4fd9b08be 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -192,8 +192,6 @@ namespace sat {
             return;
         if (!m_subsumption && !bce_enabled() && !bca_enabled() && !elim_vars_enabled())
             return;
-
-        // solver::scoped_disable_checkpoint _scoped_disable_checkpoint(s);
         
         initialize();
 
@@ -257,7 +255,6 @@ namespace sat {
         TRACE("sat_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout););
 
         finalize();
-
     }
 
     /**
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index c55383a57..09fe08f18 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -530,7 +530,6 @@ namespace sat {
     }
 
     void solver::defrag_clauses() {
-        return;
         if (memory_pressure()) return;
         pop(scope_lvl());
         IF_VERBOSE(1, verbose_stream() << "(sat-defrag)\n");
@@ -802,9 +801,9 @@ namespace sat {
         
         if (m_config.m_propagate_prefetch) {
 #if defined(__GLUC__) || defined(__clang__)
-            __builtin_prefetch((const char*)(&*(m_watches[l.index()].c_ptr())));
+            __builtin_prefetch((const char*)((m_watches[l.index()].c_ptr())));
 #else
-            _mm_prefetch((const char*)(&*(m_watches[l.index()].c_ptr())), _MM_HINT_T1);
+            _mm_prefetch((const char*)((m_watches[l.index()].c_ptr())), _MM_HINT_T1);
 #endif
         }