diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
index 073110077..d5ea181c4 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -802,7 +802,7 @@ namespace sat {
 
     //
     // placeholder for trim function.
-    // 1. forward pass replaying propositional proof, populate trail stack.
+    // 1. trail contains justification for the empty clause.
     // 2. backward pass to prune.
     // 
     svector<std::pair<clause&, status>> drat::trim() {
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 9d84d8439..f8f187fc2 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -945,8 +945,8 @@ namespace sat {
         if (j.level() == 0) {
             if (m_config.m_drat) 
                 drat_log_unit(l, j);
-            
-            j = justification(0); // erase justification for level 0
+            if (!m_config.m_drup_trim)
+                j = justification(0); // erase justification for level 0
         }
         else {
             VERIFY(!at_base_lvl());