diff --git a/src/ast/rewriter/str_rewriter.cpp b/src/ast/rewriter/str_rewriter.cpp
index db3885f28..875343655 100644
--- a/src/ast/rewriter/str_rewriter.cpp
+++ b/src/ast/rewriter/str_rewriter.cpp
@@ -410,6 +410,25 @@ br_status str_rewriter::mk_str_to_int(expr * arg0, expr_ref & result) {
 
 }
 
+br_status str_rewriter::mk_str_from_int(expr * arg0, expr_ref & result) {
+    TRACE("t_str_rw", tout << "rewrite (str.from-int " << mk_pp(arg0, m()) << ")" << std::endl;);
+    rational arg0Int;
+    if (m_autil.is_numeral(arg0, arg0Int)) {
+        // (str.from-int N) with N non-negative is the corresponding string in decimal notation.
+        // otherwise it is the empty string
+        if (arg0Int.is_nonneg()) {
+            std::string str = arg0Int.to_string();
+            result = m_strutil.mk_string(str);
+            TRACE("t_str_rw", tout << "convert non-negative integer constant to " << str << std::endl;);
+        } else {
+            result = m_strutil.mk_string("");
+            TRACE("t_str_rw", tout << "convert invalid integer constant to empty string" << std::endl;);
+        }
+        return BR_DONE;
+    }
+    return BR_FAILED;
+}
+
 br_status str_rewriter::mk_str_Substr(expr * base, expr * start, expr * len, expr_ref & result) {
     TRACE("t_str_rw", tout << "rewrite (Substr " << mk_pp(base, m()) << " " << mk_pp(start, m()) << " " << mk_pp(len, m()) << ")" << std::endl;);
     rational startVal, lenVal;
@@ -559,6 +578,9 @@ br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_STR_STR2INT:
     	SASSERT(num_args == 1);
     	return mk_str_to_int(args[0], result);
+    case OP_STR_INT2STR:
+        SASSERT(num_args == 1);
+        return mk_str_from_int(args[0], result);
     case OP_STR_SUBSTR:
         SASSERT(num_args == 3);
         return mk_str_Substr(args[0], args[1], args[2], result);
diff --git a/src/ast/rewriter/str_rewriter.h b/src/ast/rewriter/str_rewriter.h
index 10898eae7..822fb1ea8 100644
--- a/src/ast/rewriter/str_rewriter.h
+++ b/src/ast/rewriter/str_rewriter.h
@@ -54,6 +54,7 @@ public:
     br_status mk_str_Replace(expr * base, expr * source, expr * target, expr_ref & result);
     br_status mk_str_Substr(expr * base, expr * start, expr * len, expr_ref & result);
     br_status mk_str_to_int(expr * arg0, expr_ref & result);
+    br_status mk_str_from_int(expr * arg0, expr_ref & result);
 
     br_status mk_re_Str2Reg(expr * str, expr_ref & result);
     br_status mk_re_RegexIn(expr * str, expr * re, expr_ref & result);
diff --git a/src/ast/str_decl_plugin.cpp b/src/ast/str_decl_plugin.cpp
index 333ae2a02..4f9dcb7aa 100644
--- a/src/ast/str_decl_plugin.cpp
+++ b/src/ast/str_decl_plugin.cpp
@@ -37,6 +37,7 @@ str_decl_plugin::str_decl_plugin():
     m_substr_decl(0),
     m_replace_decl(0),
 	m_str2int_decl(0),
+	m_int2str_decl(0),
 	m_re_str2regex_decl(0),
 	m_re_regexin_decl(0),
 	m_re_regexconcat_decl(0),
@@ -69,6 +70,7 @@ void str_decl_plugin::finalize(void) {
     DEC_REF(m_substr_decl);
     DEC_REF(m_replace_decl);
     DEC_REF(m_str2int_decl);
+    DEC_REF(m_int2str_decl);
     DEC_REF(m_re_str2regex_decl);
     DEC_REF(m_re_regexin_decl);
     DEC_REF(m_re_regexconcat_decl);
@@ -150,6 +152,9 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) {
     m_str2int_decl = m->mk_func_decl(symbol("str.to-int"), s, i, func_decl_info(id, OP_STR_STR2INT));
     m_manager->inc_ref(m_str2int_decl);
 
+    m_int2str_decl = m->mk_func_decl(symbol("str.from-int"), i, s, func_decl_info(id, OP_STR_INT2STR));
+    m_manager->inc_ref(m_int2str_decl);
+
     m_re_str2regex_decl = m->mk_func_decl(symbol("Str2Reg"), s, re, func_decl_info(id, OP_RE_STR2REGEX));
     m_manager->inc_ref(m_re_str2regex_decl);
 
@@ -202,6 +207,7 @@ func_decl * str_decl_plugin::mk_func_decl(decl_kind k) {
     case OP_STR_SUBSTR: return m_substr_decl;
     case OP_STR_REPLACE: return m_replace_decl;
     case OP_STR_STR2INT: return m_str2int_decl;
+    case OP_STR_INT2STR: return m_int2str_decl;
     case OP_RE_STR2REGEX: return m_re_str2regex_decl;
     case OP_RE_REGEXIN: return m_re_regexin_decl;
     case OP_RE_REGEXCONCAT: return m_re_regexconcat_decl;
@@ -276,6 +282,7 @@ void str_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol cons
     op_names.push_back(builtin_name("Substring", OP_STR_SUBSTR));
     op_names.push_back(builtin_name("Replace", OP_STR_REPLACE));
     op_names.push_back(builtin_name("str.to-int", OP_STR_STR2INT));
+    op_names.push_back(builtin_name("str.from-int", OP_STR_INT2STR));
     op_names.push_back(builtin_name("Str2Reg", OP_RE_STR2REGEX));
     op_names.push_back(builtin_name("RegexIn", OP_RE_REGEXIN));
     op_names.push_back(builtin_name("RegexConcat", OP_RE_REGEXCONCAT));
diff --git a/src/ast/str_decl_plugin.h b/src/ast/str_decl_plugin.h
index e9ab43865..29b2ce9c3 100644
--- a/src/ast/str_decl_plugin.h
+++ b/src/ast/str_decl_plugin.h
@@ -43,6 +43,7 @@ enum str_op_kind {
     OP_STR_REPLACE,
 	// string-integer conversion
 	OP_STR_STR2INT,
+	OP_STR_INT2STR,
 	// regular expression operators
 	OP_RE_STR2REGEX,
 	OP_RE_REGEXIN,
@@ -76,6 +77,7 @@ protected:
     func_decl * m_substr_decl;
     func_decl * m_replace_decl;
     func_decl * m_str2int_decl;
+    func_decl * m_int2str_decl;
 
     func_decl * m_re_str2regex_decl;
     func_decl * m_re_regexin_decl;