diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
index c0799c061..f8e04a583 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -120,22 +120,27 @@ namespace sat {
         case status::deleted: ch = 'd'; break;
         default: UNREACHABLE(); break;
         }
-        (*m_bout) << ch;
+        char buffer[10000];
+        int len = 0;
+        buffer[len++] = ch;
 
         for (unsigned i = 0; i < n; ++i) {
             literal lit = c[i];
             unsigned v = 2 * lit.var() + (lit.sign() ? 1 : 0);
             do {
-                ch = static_cast<unsigned char>(v & ((1 << 7) - 1));
+                ch = static_cast<unsigned char>(v & 255);
                 v >>= 7;
-                if (v) ch |= (1 << 7);
-                //std::cout << std::hex << ((unsigned char)ch) << std::dec << " ";
-                (*m_bout) << ch;
+                if (v) ch |= 128;
+                buffer[len++] = ch;
+                if (len == sizeof(buffer)) {
+                    m_bout->write(buffer, len);
+                    len = 0;
+                }
             }
             while (v);
         }
-        ch = 0;
-        (*m_bout) << ch;
+        buffer[len++] = 0;
+        m_bout->write(buffer, len);
     }
 
     bool drat::is_cleaned(clause& c) const {
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index f536dda03..58dab0ff5 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -1222,7 +1222,6 @@ namespace sat {
            RI literals.
          */
         void minimize_covered_clause(unsigned idx) {
-            literal _blocked = m_covered_clause[idx];
             for (literal l : m_tautology) VERIFY(s.is_marked(l));
             for (literal l : m_covered_clause) s.unmark_visited(l);
             for (literal l : m_tautology) s.mark_visited(l);