mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

fix #5108

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-03-16 07:36:58 -07:00
parent d0515dca50
commit 9c716a2788
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/rewriter/seq_rewriter.cpp
View file

@ -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) { 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_concat(as.size() - 1, as.c_ptr() + 1, as[0]->get_sort());
result = str().mk_stoi(result); result = m().mk_ite(str().mk_is_empty(result),
result = m().mk_ite(m_autil.mk_lt(result, m_autil.mk_int(0)),
m_autil.mk_int(0), m_autil.mk_int(0),
result); str().mk_stoi(result));
return BR_REWRITE_FULL; return BR_REWRITE_FULL;
} }