diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
index aa5ddd6cf..ee0e4cced 100644
--- a/src/ast/sls/sls_arith_base.cpp
+++ b/src/ast/sls/sls_arith_base.cpp
@@ -2476,7 +2476,10 @@ namespace sls {
             return ctx.get_value(e->get_arg(0)) == ctx.get_value(e->get_arg(1));            
         case OP_DISTINCT:
             return false;
+        case OP_ITE:
+            return get_bool_value(e->get_arg(0)) ? get_bool_value(e->get_arg(1)) : get_bool_value(e->get_arg(2));
         default:
+            verbose_stream() << mk_pp(e, m) << "\n";
             NOT_IMPLEMENTED_YET();
         }
         return false;
diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp
index 6ac67663a..006f40b22 100644
--- a/src/smt/dyn_ack.cpp
+++ b/src/smt/dyn_ack.cpp
@@ -431,6 +431,7 @@ namespace smt {
         justification * js = nullptr;
         if (m.proofs_enabled())
             js = alloc(dyn_ack_cc_justification, n1, n2);
+        verbose_stream() << "dynack-clause\n";
         clause * cls = m_context.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA, del_eh);
         if (!cls) {
             dealloc(del_eh);
@@ -490,6 +491,7 @@ namespace smt {
         ctx.mark_as_relevant(eq1);
         ctx.mark_as_relevant(eq2);
         ctx.mark_as_relevant(eq3);
+        verbose_stream() << "dynack-transitivity\n";
         clause * cls = ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA, del_eh);
         if (!cls) {
             dealloc(del_eh);
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 42ef58acf..cc1775153 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3438,6 +3438,7 @@ public:
             VERIFY(validate_conflict());
         if (params().m_arith_dump_lemmas)
             dump_conflict();
+
         if (is_conflict) {
             ctx().set_conflict(
                 ctx().mk_justification(
@@ -3751,19 +3752,22 @@ public:
         }
     };
 
+    unsigned m_num_dumped_lemmas = 0;
+
     void dump_assign_lemma(literal lit) {
-        m_core.push_back(~lit);
+        std::cout << "; assign lemma " << (m_num_dumped_lemmas++) << "\n";
         ctx().display_lemma_as_smt_problem(std::cout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), lit);
-        m_core.pop_back();
         std::cout << "(reset)\n";
     }
 
     void dump_conflict() {
+        std::cout << "; conflict " << (m_num_dumped_lemmas++) << "\n";
         ctx().display_lemma_as_smt_problem(std::cout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data());
         std::cout << "(reset)\n";
     }
 
     void dump_eq(enode* x, enode* y) {
+        std::cout << "; equality propagation " << (m_num_dumped_lemmas++) << "\n";
         ctx().display_lemma_as_smt_problem(std::cout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), false_literal, symbol::null, x, y);
         std::cout << "(reset)\n";
     }