diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index c6d51b1a4..568e6b5ae 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -26,7 +26,8 @@ namespace smt {
 theory_str::theory_str(ast_manager & m):
         theory(m.mk_family_id("str")),
         search_started(false),
-        m_autil(m)
+        m_autil(m),
+        m_strutil(m)
 {
 }
 
@@ -100,8 +101,15 @@ bool theory_str::internalize_term(app * term) {
 }
 
 app * theory_str::mk_strlen(app * e) {
-    expr * args[1] = {e};
-    return get_manager().mk_app(get_id(), OP_STRLEN, 0, 0, 1, args);
+    if (m_strutil.is_string(e)) {
+        const char * strval = 0;
+        m_strutil.is_string(e, &strval);
+        int len = strlen(strval);
+        return m_autil.mk_numeral(rational(len), true);
+    } else {
+        expr * args[1] = {e};
+        return get_manager().mk_app(get_id(), OP_STRLEN, 0, 0, 1, args);
+    }
 }
 
 /*
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 867c4316b..a583a106e 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -34,6 +34,8 @@ namespace smt {
         // TODO
     protected:
         bool search_started;
+        arith_util m_autil;
+        str_util m_strutil;
     protected:
         virtual bool internalize_atom(app * atom, bool gate_ctx);
         virtual bool internalize_term(app * term);
@@ -61,7 +63,6 @@ namespace smt {
     public:
         theory_str(ast_manager & m);
         virtual ~theory_str();
-        arith_util m_autil;
     protected:
         void attach_new_th_var(enode * n);
     };