From 9c716a27888cce8b6a999c771b80707f7fb92b0b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 16 Mar 2021 07:36:58 -0700 Subject: [PATCH] fix #5108 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index d36861ea8..a90b193f9 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2306,10 +2306,9 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) { } if (str().is_unit(as.get(0), u) && m_util.is_const_char(u, ch) && '0' == ch) { result = str().mk_concat(as.size() - 1, as.c_ptr() + 1, as[0]->get_sort()); - result = str().mk_stoi(result); - result = m().mk_ite(m_autil.mk_lt(result, m_autil.mk_int(0)), + result = m().mk_ite(str().mk_is_empty(result), m_autil.mk_int(0), - result); + str().mk_stoi(result)); return BR_REWRITE_FULL; }