diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 533d9f09f..fc38f0ae4 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1103,7 +1103,7 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) { } expr* b; if (m_util.str.is_itos(a, b)) { - result = b; + result = m().mk_ite(m_autil.mk_ge(b, m_autil.mk_int(0)), b, m_autil.mk_int(-1)); return BR_DONE; } return BR_FAILED;