diff --git a/src/ast/euf/euf_etable.cpp b/src/ast/euf/euf_etable.cpp
index 17be983fe..d79944c9b 100644
--- a/src/ast/euf/euf_etable.cpp
+++ b/src/ast/euf/euf_etable.cpp
@@ -224,11 +224,6 @@ namespace euf {
     void etable::erase(enode * n) {
         SASSERT(n->num_args() > 0);
         void * t = get_table(n); 
-        static unsigned count = 0;
-        //verbose_stream() << "erase " << (++count) << " " << n << "\n";
-        // if (count == 10398) {
-        //     verbose_stream() << "here\n";
-        // }
         switch (static_cast<table_kind>(GET_TAG(t))) {
         case UNARY:
             UNTAG(unary_table*, t)->erase(n);
diff --git a/src/sat/sat_ddfw.cpp b/src/sat/sat_ddfw.cpp
index ca274be51..f15c241f2 100644
--- a/src/sat/sat_ddfw.cpp
+++ b/src/sat/sat_ddfw.cpp
@@ -494,7 +494,7 @@ namespace sat {
         unsigned h = value_hash();
         unsigned occs = 0;
         bool contains = m_models.find(h, occs);
-        if (!m_models.contains(h)) {
+        if (!contains) {
             for (unsigned v = 0; v < num_vars(); ++v)
                 bias(v) += value(v) ? 1 : -1;
             if (m_models.size() > m_config.m_max_num_models)
diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp
index 783f268bd..e621ee9d7 100644
--- a/src/sat/smt/arith_diagnostics.cpp
+++ b/src/sat/smt/arith_diagnostics.cpp
@@ -199,6 +199,9 @@ namespace arith {
             name = "implied-eq";
             args.push_back(arith.mk_int(m_num_le));
             break;
+        default:
+            name = "unknown-arithmetic";
+            break;
         }
         rational lc(1);
         for (unsigned i = m_lit_head; i < m_lit_tail; ++i)