diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index 035e228fb..0006d508c 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -298,6 +298,18 @@ format * smt2_pp_environment::mk_float(rational const & val) const {
     return mk_string(get_manager(), s.c_str());
 }
 
+format * smt2_pp_environment::pp_str_literal(app * t) {
+    TRACE("parse_string", tout << "pp_str_literal\n";);
+    str_util & u = get_strutil();
+    SASSERT(u.is_string(t));
+    const char * val;
+    u.is_string(t, &val);
+    ast_manager & m = get_manager();
+    string_buffer<> buf;
+    buf << "\"" << val << "\"";
+    return mk_string(m, buf.c_str());
+}
+
 format * smt2_pp_environment::pp_arith_literal(app * t, bool decimal, unsigned decimal_prec) {
     arith_util & u = get_autil();
     SASSERT(u.is_numeral(t) || u.is_irrational_algebraic_numeral(t));
@@ -581,6 +593,9 @@ class smt2_printer {
         else if (m_env.get_dlutil().is_numeral(c)) {
             f = m_env.pp_datalog_literal(c);
         }
+        else if (m_env.get_strutil().is_string(c)) {
+            f = m_env.pp_str_literal(c);
+        }
         else {
             buffer<symbol> names;
             if (m().is_label_lit(c, names)) {
diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h
index 8aac71b8c..17bc322bc 100644
--- a/src/ast/ast_smt2_pp.h
+++ b/src/ast/ast_smt2_pp.h
@@ -29,6 +29,7 @@ Revision History:
 #include"array_decl_plugin.h"
 #include"fpa_decl_plugin.h"
 #include"dl_decl_plugin.h"
+#include"str_decl_plugin.h"
 #include"smt2_util.h"
 
 class smt2_pp_environment {
@@ -47,12 +48,14 @@ public:
     virtual bv_util & get_bvutil() = 0;
     virtual array_util & get_arutil() = 0;
     virtual fpa_util & get_futil() = 0;
+    virtual str_util & get_strutil() = 0;
     virtual datalog::dl_decl_util& get_dlutil() = 0;
     virtual bool uses(symbol const & s) const = 0; 
     virtual format_ns::format * pp_fdecl(func_decl * f, unsigned & len);
     virtual format_ns::format * pp_bv_literal(app * t, bool use_bv_lits, bool bv_neg);
     virtual format_ns::format * pp_arith_literal(app * t, bool decimal, unsigned prec);
     virtual format_ns::format * pp_float_literal(app * t, bool use_bv_lits, bool use_float_real_lits);
+    virtual format_ns::format * pp_str_literal(app * t);
     virtual format_ns::format * pp_datalog_literal(app * t);
     virtual format_ns::format * pp_sort(sort * s);
     virtual format_ns::format * pp_fdecl_ref(func_decl * f);
@@ -70,14 +73,16 @@ class smt2_pp_environment_dbg : public smt2_pp_environment {
     bv_util       m_bvutil;
     array_util    m_arutil;
     fpa_util      m_futil;
+    str_util      m_strutil;
     datalog::dl_decl_util m_dlutil;
 public:
-    smt2_pp_environment_dbg(ast_manager & m):m_manager(m), m_autil(m), m_bvutil(m), m_arutil(m), m_futil(m), m_dlutil(m) {}
+    smt2_pp_environment_dbg(ast_manager & m):m_manager(m), m_autil(m), m_bvutil(m), m_arutil(m), m_futil(m), m_strutil(m), m_dlutil(m) {}
     virtual ast_manager & get_manager() const { return m_manager; }
     virtual arith_util & get_autil() { return m_autil; }
     virtual bv_util & get_bvutil() { return m_bvutil; }
     virtual array_util & get_arutil() { return m_arutil; }
     virtual fpa_util & get_futil() { return m_futil; }
+    virtual str_util & get_strutil() { return m_strutil; }
     virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; }
     virtual bool uses(symbol const & s) const { return false; }
 };
diff --git a/src/ast/str_decl_plugin.cpp b/src/ast/str_decl_plugin.cpp
index 66b6c23fc..3bd81970d 100644
--- a/src/ast/str_decl_plugin.cpp
+++ b/src/ast/str_decl_plugin.cpp
@@ -74,6 +74,11 @@ bool str_recognizers::is_string(expr const * n, const char ** val) const {
     return true;
 }
 
+bool str_recognizers::is_string(expr const * n) const {
+    const char * tmp = 0;
+    return is_string(n, & tmp);
+}
+
 str_util::str_util(ast_manager &m) :
     str_recognizers(m.mk_family_id(symbol("str"))),
     m_manager(m) {
diff --git a/src/ast/str_decl_plugin.h b/src/ast/str_decl_plugin.h
index 2d629e006..57829d542 100644
--- a/src/ast/str_decl_plugin.h
+++ b/src/ast/str_decl_plugin.h
@@ -57,6 +57,7 @@ public:
     family_id get_family_id() const { return get_fid(); }
 
     bool is_string(expr const * n, const char ** val) const;
+    bool is_string(expr const * n) const;
     // TODO
 };
 
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 0c60d876b..77cbfe132 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -25,6 +25,7 @@ Notes:
 #include"datatype_decl_plugin.h"
 #include"seq_decl_plugin.h"
 #include"fpa_decl_plugin.h"
+#include"str_decl_plugin.h"
 #include"ast_pp.h"
 #include"var_subst.h"
 #include"pp.h"
@@ -241,6 +242,7 @@ protected:
     bv_util       m_bvutil;
     array_util    m_arutil;
     fpa_util      m_futil;
+    str_util      m_strutil;
     datalog::dl_decl_util m_dlutil;
 
     format_ns::format * pp_fdecl_name(symbol const & s, func_decls const & fs, func_decl * f, unsigned & len) {
@@ -261,13 +263,14 @@ protected:
     }
 
 public:
-    pp_env(cmd_context & o):m_owner(o), m_autil(o.m()), m_bvutil(o.m()), m_arutil(o.m()), m_futil(o.m()), m_dlutil(o.m()) {}
+    pp_env(cmd_context & o):m_owner(o), m_autil(o.m()), m_bvutil(o.m()), m_arutil(o.m()), m_futil(o.m()), m_strutil(o.m()), m_dlutil(o.m()) {}
     virtual ~pp_env() {}
     virtual ast_manager & get_manager() const { return m_owner.m(); }
     virtual arith_util & get_autil() { return m_autil; }
     virtual bv_util & get_bvutil() { return m_bvutil; }
     virtual array_util & get_arutil() { return m_arutil; }
     virtual fpa_util & get_futil() { return m_futil; }
+    virtual str_util & get_strutil() { return m_strutil; }
     virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; }
     virtual bool uses(symbol const & s) const { 
         return