From cb140011bc9a574950a185ee29011d494001f944 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 10 Sep 2016 09:42:36 -0700
Subject: [PATCH] add missing rewrite rule. Issue #731

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_rewriter.cpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index d36f61a85..0907ff4c7 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -890,6 +890,11 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
         result = m_autil.mk_numeral(r, true);
         return BR_DONE;
     }
+    expr* b;
+    if (m_util.str.is_itos(a, b)) {
+        result = b;
+        return BR_DONE;
+    }
     return BR_FAILED;
 }