diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index cdcee87f3..9bcb856f6 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -631,6 +631,7 @@ void seq_decl_plugin::init() {
 #endif
     m_sigs[_OP_STRING_STRIDOF]   = alloc(psig, m, "str.indexof", 0, 3, str2TintT, intT);
     m_sigs[_OP_STRING_STRREPL]   = alloc(psig, m, "str.replace", 0, 3, str3T, strT);
+    m_sigs[_OP_STRING_FROM_CHAR] = alloc(psig, m, "char", 1, 0, nullptr, strT);
     m_sigs[OP_STRING_ITOS]       = alloc(psig, m, "str.from_int", 0, 1, &intT, strT);
     m_sigs[OP_STRING_STOI]       = alloc(psig, m, "str.to_int", 0, 1, &strT, intT);
     m_sigs[OP_STRING_LT]         = alloc(psig, m, "str.<", 0, 2, str2T, boolT);
@@ -867,6 +868,14 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case _OP_STRING_CONCAT:
         return mk_assoc_fun(k, arity, domain, range, OP_SEQ_CONCAT, k);
 
+    case _OP_STRING_FROM_CHAR: {
+        if (!(num_parameters == 1 && parameters[0].is_int())) 
+            m.raise_exception("character literal expects integer parameter");
+        zstring zs(parameters[0].get_int());        
+        parameter p(zs.encode().c_str());
+        return m.mk_const_decl(m_stringc_sym, m_string,func_decl_info(m_family_id, OP_STRING_CONST, 1, &p));
+    }
+        
     case OP_SEQ_REPLACE:
         return mk_seq_fun(k, arity, domain, range, _OP_STRING_STRREPL);
     case _OP_STRING_STRREPL:
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 39c09287f..d131bfeb7 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -94,6 +94,7 @@ enum seq_op_kind {
     OP_CHAR_LE,       // Unicode comparison
 #endif
     // internal only operators. Converted to SEQ variants.
+    _OP_STRING_FROM_CHAR,
     _OP_STRING_STRREPL,
     _OP_STRING_CONCAT,
     _OP_STRING_LENGTH,
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 085e6298a..b58c3cd3b 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -408,6 +408,7 @@ namespace smt2 {
         bool curr_is_rparen() const { return curr() == scanner::RIGHT_PAREN; }
         bool curr_is_int() const { return curr() == scanner::INT_TOKEN; }
         bool curr_is_float() const { return curr() == scanner::FLOAT_TOKEN; }
+        bool curr_is_bv() const { return curr() == scanner::BV_TOKEN; }
 
         bool curr_id_is_underscore() const { SASSERT(curr_is_identifier()); return curr_id() == m_underscore; }
         bool curr_id_is_as() const { SASSERT(curr_is_identifier()); return curr_id() == m_as; }
@@ -1551,7 +1552,7 @@ namespace smt2 {
             symbol r = curr_id();
             next();
             while (!curr_is_rparen()) {
-                if (curr_is_int()) {
+                if (curr_is_int() || curr_is_bv()) {
                     if (!curr_numeral().is_unsigned()) {
                         m_param_stack.push_back(parameter(curr_numeral()));                       
                     }