prepare ground for drup trim

By not deleting justifications in base level unit literals it is possible for drup-trim to inspect the trail for dependencies - which clauses were used to derive a literal.

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() {

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());