diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
index 110ad3b8a..e7b9088d5 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -483,10 +483,6 @@ namespace sat {
                     literal lit = c[i];
                     if (lit != wc.m_l1 && lit != wc.m_l2 && value(lit) != l_false) {
                         wc.m_l2 = lit;
-						if (m_watches.size() <= (~lit).index())
-						{
-							IF_VERBOSE(0, verbose_stream() << m_watches.size() << " " << lit << " " << (~lit).index() << "\n");
-						}
                         m_watches[(~lit).index()].push_back(idx);
                         done = true;
                     } 
diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp
index 52ab9f9f7..e76a3f7c4 100644
--- a/src/sat/sat_probing.cpp
+++ b/src/sat/sat_probing.cpp
@@ -65,6 +65,10 @@ namespace sat {
         if (implied_lits) {
             for (literal lit : *implied_lits) {
                 if (m_assigned.contains(lit)) {
+                    if (s.m_config.m_drat) {
+                        s.m_drat.add(l, lit, true);
+                        s.m_drat.add(~l, lit, true);
+                    }
                     s.assign(lit, justification());
                     m_num_assigned++;
                 }
@@ -95,8 +99,12 @@ namespace sat {
                 cache_bins(l, old_tr_sz);
             s.pop(1);
 
-            for (literal l : m_to_assert) {
-                s.assign(l, justification());
+            for (literal lit : m_to_assert) {
+                if (s.m_config.m_drat) {
+                    s.m_drat.add(l, lit, true);
+                    s.m_drat.add(~l, lit, true);
+                }
+                s.assign(lit, justification());
                 m_num_assigned++;
             }
         }