diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 1b1d6c450..40c238cb7 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -36,6 +36,7 @@ expr_ref sym_expr::accept(expr* e) {
         break;
     }
     case t_char:
+        SASSERT(m.get_sort(e) == m.get_sort(m_t));
         result = m.mk_eq(e, m_t);
         break;
     case t_range: {
@@ -792,8 +793,8 @@ bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
         else if (m_util.str.is_empty(e)) {
             continue;
         }
-        else if (m_util.str.is_unit(e)) {
-            seq.push_back(e);
+        else if (m_util.str.is_unit(e, e1)) {
+            seq.push_back(e1);
         }
         else if (m_util.str.is_concat(e, e1, e2)) {
             todo.push_back(e1);
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index f15e83381..0eac9d316 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -31,6 +31,10 @@ static bool is_hex_digit(char ch, unsigned& d) {
         d = 10 + ch - 'A';
         return true;
     }
+    if ('a' <= ch && ch <= 'f') {
+        d = 10 + ch - 'a';
+        return true;
+    }
     return false;
 }
 
@@ -85,6 +89,7 @@ static bool is_escape_char(char const *& s, unsigned& result) {
         s += 2;
         return true;
     }
+    return false;
 }
 
 zstring::zstring(encoding enc): m_encoding(enc) {}
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 8a40f9d7a..9f7656471 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -847,6 +847,9 @@ namespace smt {
                 setup_AUFLIA(false);
             setup_datatypes();
             setup_bv();
+            setup_dl();
+            setup_seq();
+            setup_card();
             setup_fpa();
             return;
         }