diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 205f0484a..47d5fbfae 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -839,7 +839,7 @@ namespace smt {
 
         void mk_ite_cnstr(app * n);
 
-        void dec_ref(literal l) { SASSERT(m_lit_occs[l.index()] > 0); m_lit_occs[l.index()]--; }
+        void dec_ref(literal l) { if (m_lit_occs[l.index()] > 0) m_lit_occs[l.index()]--; }
 
         void inc_ref(literal l) { m_lit_occs[l.index()]++; }
 
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 80482a99c..ea4787c02 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1373,6 +1373,15 @@ namespace smt {
             break;
         }
         TRACE("mk_clause", tout << "after simplification:\n"; display_literals_verbose(tout, num_lits, lits) << "\n";);
+#if 0
+        for (unsigned i = 0; i < num_lits; ++i) {
+            expr_ref tmp(m);
+            literal2expr(lits[i], tmp);
+            std::cout << tmp << "\n";
+        }
+        std::cout << "\n";
+#endif
+
         unsigned activity = 0;
         if (activity == 0)
             activity = 1;