diff --git a/src/ast/rewriter/char_rewriter.cpp b/src/ast/rewriter/char_rewriter.cpp
index 5d730d7c6..14b86773a 100644
--- a/src/ast/rewriter/char_rewriter.cpp
+++ b/src/ast/rewriter/char_rewriter.cpp
@@ -18,6 +18,8 @@ Author:
 #include "util/debug.h"
 #include "ast/rewriter/char_rewriter.h"
 #include "ast/bv_decl_plugin.h"
+#include "ast/arith_decl_plugin.h"
+
 
 char_rewriter::char_rewriter(ast_manager& m):
     m(m) {
@@ -37,6 +39,7 @@ br_status char_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * co
     case OP_CHAR_LE:
         break;
     case OP_CHAR_TO_INT:
+        st = mk_char_to_int(args[0], result);        
         break;
     case OP_CHAR_TO_BV:
         break;
@@ -52,11 +55,19 @@ br_status char_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * co
 br_status char_rewriter::mk_char_from_bv(expr* e, expr_ref& result) {
     bv_util bv(m);
     rational n;
-    if (bv.is_numeral(e, n) && n.is_unsigned()) {
-        if (n > m_char->max_char())
-            return BR_FAILED;
+    if (bv.is_numeral(e, n) && n.is_unsigned() && n <= m_char->max_char()) {
         result = m_char->mk_char(n.get_unsigned());
         return BR_DONE;
     }
     return BR_FAILED;
 }
+
+br_status char_rewriter::mk_char_to_int(expr* e, expr_ref& result) {
+    unsigned n = 0;
+    if (m_char->is_const_char(e, n)) {
+        arith_util arith(m);
+        result = arith.mk_int(n);
+        return BR_DONE;
+    }
+    return BR_FAILED;
+}
diff --git a/src/ast/rewriter/char_rewriter.h b/src/ast/rewriter/char_rewriter.h
index f8e3b909e..f67695bd8 100644
--- a/src/ast/rewriter/char_rewriter.h
+++ b/src/ast/rewriter/char_rewriter.h
@@ -32,6 +32,9 @@ class char_rewriter {
     char_decl_plugin* m_char;
 
     br_status mk_char_from_bv(expr* e, expr_ref& result);
+
+    br_status mk_char_to_int(expr* e, expr_ref& result);
+
 public:
 
     char_rewriter(ast_manager& m);