diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index d8a6c47bc..d138685ed 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -2991,7 +2991,10 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
           for (unsigned i = 0; i < num_proofs; i++) tout << mk_pp(get_fact(proofs[i]), *this) << "\n";
           tout << "===>\n";
           tout << mk_pp(new_fact, *this) << "\n";);
-        SASSERT(num_proofs == cls_sz || (num_proofs == cls_sz + 1 && is_false(new_fact)));
+        //
+        // typically: num_proofs == cls_sz || (num_proofs == cls_sz + 1 && is_false(new_fact))
+        // but formula could have repeated literals that are merged in the clausal representation.
+        //
         unsigned num_matches = 0;
         for (unsigned i = 0; i < cls_sz; i++) {
             expr * lit = cls->get_arg(i);
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 45bd75ab7..a17271e4e 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1045,15 +1045,13 @@ namespace smt {
     bool context::simplify_aux_clause_literals(unsigned & num_lits, literal * lits, literal_buffer & simp_lits) {
         std::sort(lits, lits + num_lits);
         literal prev = null_literal;
-        unsigned i = 0;
         unsigned j = 0;
-        for (; i < num_lits; i++) {
+        for (unsigned i = 0; i < num_lits; i++) {
             literal curr = lits[i];
             lbool   val  = get_assignment(curr);
-            if (val == l_false)
-                simp_lits.push_back(~curr);
             switch(val) {
             case l_false:
+                simp_lits.push_back(~curr);
                 break; // ignore literal
             case l_undef:
                 if (curr == ~prev)
@@ -1295,8 +1293,9 @@ namespace smt {
                     SASSERT(get_assignment(simp_lits[i]) == l_true);
                 }
             });
-            if (old_num_lits != num_lits) 
+            if (!simp_lits.empty()) {
                 j = mk_justification(unit_resolution_justification(m_region, j, simp_lits.size(), simp_lits.c_ptr()));
+            }
             break;
         }
         case CLS_AUX_LEMMA: {
diff --git a/src/smt/smt_justification.cpp b/src/smt/smt_justification.cpp
index de3594fcc..c091f6973 100644
--- a/src/smt/smt_justification.cpp
+++ b/src/smt/smt_justification.cpp
@@ -52,6 +52,7 @@ namespace smt {
                   tout << lits[i] << " ";
               }
               tout << "\n";);
+        SASSERT(m_num_literals > 0);
     }
 
     unit_resolution_justification::unit_resolution_justification(justification * js, 
@@ -68,6 +69,7 @@ namespace smt {
                   tout << lits[i] << " ";
               }
               tout << "\n";);
+        SASSERT(num_lits != 0);
     }
 
     unit_resolution_justification::~unit_resolution_justification() {