diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 4fcfb982c..01f4f924f 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -440,20 +440,16 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
  * (seq.unit (_ BitVector 8)) ==> String constant
  */
 br_status seq_rewriter::mk_seq_unit(expr* e, expr_ref& result) {
-    sort * s = m().get_sort(e);
     bv_util bvu(m());
-
-    if (is_sort_of(s, bvu.get_family_id(), BV_SORT)) {
-        // specifically we want (_ BitVector 8)
-        rational n_val;
-        unsigned int n_size;
-        if (bvu.is_numeral(e, n_val, n_size) && n_size == 8) {
-            // convert to string constant
-            zstring str(n_val.get_unsigned());
-            TRACE("seq", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << str<< "\"" << std::endl;);
-            result = m_util.str.mk_string(str);
-            return BR_DONE;
-        }
+    rational n_val;
+    unsigned int n_size;
+    // specifically we want (_ BitVector 8)
+    if (bvu.is_bv(e) && bvu.is_numeral(e, n_val, n_size) && n_size == 8) {
+        // convert to string constant
+        zstring str(n_val.get_unsigned());
+        TRACE("seq", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << str<< "\"" << std::endl;);
+        result = m_util.str.mk_string(str);
+        return BR_DONE;
     }
 
     return BR_FAILED;