diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
index 5de340674..16785d566 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -100,7 +100,7 @@ namespace sat {
                 v /= 10;
                 SASSERT(d > digits);
             }
-	    SASSERT(len + lastd - d < sizeof(buffer));
+	    SASSERT(len + lastd < sizeof(buffer) + d);
 	    memcpy(buffer + len, d, lastd - d);
 	    len += static_cast<unsigned>(lastd - d);            
 	    buffer[len++] = ' ';
diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index b1e89f72e..d44548f0b 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -439,6 +439,7 @@ void asserted_formulas::commit(unsigned new_qhead) {
         justified_expr const& j = m_formulas[i];
         update_substitution(j.get_fml(), j.get_proof());
     }
+    (void)new_sub;
     m_qhead = new_qhead;
 }