diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp
index 84b28a7a5..210f64604 100644
--- a/src/smt/dyn_ack.cpp
+++ b/src/smt/dyn_ack.cpp
@@ -431,7 +431,7 @@ namespace smt {
         justification * js = nullptr;
         if (m.proofs_enabled())
             js = alloc(dyn_ack_cc_justification, n1, n2);
-        clause * cls = m_context.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA, del_eh);
+        clause * cls = m_context.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA_RELEVANT, del_eh);
         if (!cls) {
             dealloc(del_eh);
             return;
@@ -490,7 +490,7 @@ namespace smt {
         ctx.mark_as_relevant(eq1);
         ctx.mark_as_relevant(eq2);
         ctx.mark_as_relevant(eq3);
-        clause* cls = ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA, del_eh);
+        clause* cls = ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA_RELEVANT, del_eh);
         if (!cls) {
             dealloc(del_eh);
             return;
diff --git a/src/smt/smt_clause.h b/src/smt/smt_clause.h
index 89d8f2d66..f44e7f774 100644
--- a/src/smt/smt_clause.h
+++ b/src/smt/smt_clause.h
@@ -41,11 +41,13 @@ namespace smt {
         CLS_AUX,         // an input assumption
         CLS_TH_AXIOM,    // a theory axiom
         CLS_LEARNED,     // learned through conflict resolution
-        CLS_TH_LEMMA     // a theory lemma
+        CLS_TH_LEMMA_RELEVANT,     // a theory lemma, atoms are reinitialzed as relevant for theory propagation
+        CLS_TH_LEMMA_LEARNED       // a theory lemma, lemma is replayed for Boolean propagation.
     };
 
     inline bool is_axiom(clause_kind k) { return k == CLS_AUX || k == CLS_TH_AXIOM; }
-    inline bool is_lemma(clause_kind k) { return k == CLS_LEARNED || k == CLS_TH_LEMMA; }
+    inline bool is_lemma(clause_kind k) { return k == CLS_LEARNED || k == CLS_TH_LEMMA_RELEVANT || k == CLS_TH_LEMMA_LEARNED; }
+    inline bool is_th_lemma(clause_kind k) { return k == CLS_TH_LEMMA_RELEVANT || k == CLS_TH_LEMMA_LEARNED; }
     
     /**
        \brief A SMT clause.
@@ -54,8 +56,8 @@ namespace smt {
     */
     class clause {
         unsigned m_num_literals;
-        unsigned m_capacity:24;           //!< some of the clause literals can be simplified and removed, this field contains the original number of literals (used for GC).
-        unsigned m_kind:2;                //!< kind
+        unsigned m_capacity:23;           //!< some of the clause literals can be simplified and removed, this field contains the original number of literals (used for GC).
+        unsigned m_kind:3;                //!< kind
         unsigned m_reinit:1;              //!< true if the clause is in the reinit stack (only for learned clauses and aux_lemmas)
         unsigned m_reinternalize_atoms:1; //!< true if atoms must be reinitialized during reinitialization
         unsigned m_has_atoms:1;           //!< true if the clause has memory space for storing atoms.
@@ -169,7 +171,7 @@ namespace smt {
         }
 
         bool is_th_lemma() const {
-            return get_kind() == CLS_TH_LEMMA;
+            return smt::is_th_lemma(get_kind());
         }
 
 
diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp
index 5cb3729ab..8225da0d5 100644
--- a/src/smt/smt_clause_proof.cpp
+++ b/src/smt/smt_clause_proof.cpp
@@ -51,7 +51,8 @@ namespace smt {
             return status::th_assumption;
         case CLS_LEARNED:
             return status::lemma;
-        case CLS_TH_LEMMA:
+        case CLS_TH_LEMMA_LEARNED:
+        case CLS_TH_LEMMA_RELEVANT:
             return status::th_lemma;
         default:
             UNREACHABLE();
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 2b4dc05dd..b5c923de9 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2321,7 +2321,7 @@ namespace smt {
                         });
                         literal l(v, sign);
                         cls->set_literal(j, l);
-                        if (cls->get_kind() == CLS_TH_LEMMA)
+                        if (cls->get_kind() == CLS_TH_LEMMA_RELEVANT)
                             mark_as_relevant(l);
                     }
                     SASSERT(ilvl <= m_scope_lvl);
@@ -2351,7 +2351,7 @@ namespace smt {
                     SASSERT(!cls->reinternalize_atoms());
                     literal l1 = cls->get_literal(0);
                     literal l2 = cls->get_literal(1);
-                    if (cls->get_kind() == CLS_TH_LEMMA) {
+                    if (cls->get_kind() == CLS_TH_LEMMA_RELEVANT) {
                         mark_as_relevant(l1);
                         mark_as_relevant(l2);
                     }
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index d44da1e87..55c9f1fe6 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -971,7 +971,7 @@ namespace smt {
         }
 
         void mk_th_lemma(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params = 0, parameter * params = nullptr) {
-            mk_th_clause(tid, num_lits, lits, num_params, params, CLS_TH_LEMMA);
+            mk_th_clause(tid, num_lits, lits, num_params, params, CLS_TH_LEMMA_RELEVANT);
         }
 
         void mk_th_lemma(theory_id tid, literal_vector const& ls, unsigned num_params = 0, parameter * params = nullptr) {
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 17c0033f0..abc24b5eb 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1399,7 +1399,8 @@ namespace smt {
             }            
             break;
         }
-        case CLS_TH_LEMMA:
+        case CLS_TH_LEMMA_RELEVANT:
+        case CLS_TH_LEMMA_LEARNED:
             dump_lemma(num_lits, lits);
             if (!simplify_aux_lemma_literals(num_lits, lits)) {
                 if (j && !j->in_region()) {
@@ -1474,7 +1475,7 @@ namespace smt {
                     cls->swap_lits(1, w2_idx);
                 }
                 else {
-                    SASSERT(k == CLS_TH_LEMMA);
+                    SASSERT(is_th_lemma(k));
                     int w1_idx = select_watch_lit(cls, 0);
                     cls->swap_lits(0, w1_idx);
                     int w2_idx = select_watch_lit(cls, 1);
@@ -1487,14 +1488,14 @@ namespace smt {
                 add_watch_literal(cls, 1);
                 if (get_assignment(cls->get_literal(0)) == l_false) {
                     set_conflict(b_justification(cls));
-                    if (k == CLS_TH_LEMMA && m_scope_lvl > m_base_lvl) {
+                    if (is_th_lemma(k) && m_scope_lvl > m_base_lvl) {
                         reinit     = true;
                         iscope_lvl = m_scope_lvl;
                     }
                 }
                 else if (get_assignment(cls->get_literal(1)) == l_false) {
                     assign(cls->get_literal(0), b_justification(cls));
-                    if (k == CLS_TH_LEMMA && m_scope_lvl > m_base_lvl) {
+                    if (is_th_lemma(k) && m_scope_lvl > m_base_lvl) {
                         reinit     = true;
                         iscope_lvl = m_scope_lvl;
                     }
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index e4f788f60..8dc9b2dc3 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -3008,7 +3008,7 @@ namespace smt {
             if (proofs_enabled()) 
                 js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.data(),
                            ante.num_params(), ante.params("assign-bounds"));
-            ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA, nullptr);
+            ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA_LEARNED, nullptr);
         }
         else {
             ctx.assign(l, ctx.mk_justification(
diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h
index 905f67704..44eee5593 100644
--- a/src/smt/theory_arith_int.h
+++ b/src/smt/theory_arith_int.h
@@ -677,7 +677,7 @@ namespace smt {
                 ante.eqs().size(), ante.eqs().data(), ante, l));
 
         if (l == false_literal) 
-            ctx.mk_clause(0, nullptr, js, CLS_TH_LEMMA, nullptr);
+            ctx.mk_clause(0, nullptr, js, CLS_TH_LEMMA_LEARNED, nullptr);
         else 
             ctx.assign(l, js);
         return true;
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index 807eb6cb6..7386c36ce 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -664,7 +664,7 @@ void theory_diff_logic<Ext>::new_edge(dl_var src, dl_var dst, unsigned num_edges
                    lits.size(), lits.data(), 
                    params.size(), params.data());
     }
-    ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA, nullptr);
+    ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA_LEARNED, nullptr);
 
 #if 0
     TRACE("arith",
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 1cdc8a00a..228722dcd 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2399,7 +2399,7 @@ public:
             VERIFY(validate_assign(lit));
         if (params().m_arith_dump_lemmas)
             dump_assign_lemma(lit);
-        if (false && core.size() < small_lemma_size() && eqs.empty()) {
+        if (core.size() < small_lemma_size() && eqs.empty()) {
             m_core2.reset();
             for (auto const& c : core) {
                 m_core2.push_back(~c);
@@ -2410,7 +2410,7 @@ public:
                 js = alloc(theory_lemma_justification, get_id(), ctx(), m_core2.size(), m_core2.data(),
                            ps.size(), ps.data());
             }
-            ctx().mk_clause(m_core2.size(), m_core2.data(), js, CLS_TH_LEMMA, nullptr);
+            ctx().mk_clause(m_core2.size(), m_core2.data(), js, CLS_TH_LEMMA_LEARNED, nullptr);
         }
         else {
             ctx().assign(
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index ed3ff0942..f2cdbe6c5 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -936,7 +936,7 @@ namespace smt {
             if (proofs_enabled()) {
                 js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.data());
             }
-            ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA, nullptr);
+            ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA_LEARNED, nullptr);
         }
         SASSERT(ctx.inconsistent());
     }
@@ -1518,7 +1518,7 @@ namespace smt {
         if (proofs_enabled()) {                                         
             js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.data());
         }
-        ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA, nullptr);
+        ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA_LEARNED, nullptr);
     }