diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 4c1ba3da7..24341a624 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2389,6 +2389,7 @@ namespace smt {
             assign(l, b_justification::mk_axiom());
             if (is_relevant)
                 mark_as_relevant(l);
+            verbose_stream() << "reassert " << unit << ": " << mk_bounded_pp(unit, m) << "\n";
             TRACE("reassert_units", tout << "reasserting #" << unit->get_id() << " " << sign << " @ " << m_scope_lvl << "\n";);            
         }
         if (at_base_level()) 
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index a4f8b5a09..b592742f5 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1438,8 +1438,10 @@ namespace smt {
                 m_justifications.push_back(j);
             assign(unit, j);
             inc_ref(unit);
-            if (m_scope_lvl > m_search_lvl)
+            if (m_scope_lvl > m_search_lvl && !j) {
+                verbose_stream() << "unit clause " << unit << ": " << mk_bounded_pp(atom, m) << "\n";
                 m_units_to_reassert.push_back({ expr_ref(atom, m), unit.sign(), is_relevant(unit) });
+            }
             return nullptr;
         }
         case 2: