mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

#5140

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-05-22 10:27:53 -07:00
parent a10de2e975
commit e14e3ef291
1 changed files with 10 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -4884,13 +4884,17 @@ bool seq_rewriter::reduce_itos(expr_ref_vector& ls, expr_ref_vector& rs,
str().is_itos(ls.get(0), n) && str().is_itos(ls.get(0), n) &&
is_string(rs.size(), rs.data(), s)) { is_string(rs.size(), rs.data(), s)) {
std::string s1 = s.encode(); std::string s1 = s.encode();
rational r(s1.c_str()); try {
if (s1 == r.to_string()) { rational r(s1.c_str());
eqs.push_back(n, m_autil.mk_numeral(r, true)); if (s1 == r.to_string()) {
ls.reset(); eqs.push_back(n, m_autil.mk_numeral(r, true));
rs.reset(); ls.reset();
return true; rs.reset();
return true;
}
} }
catch (...)
{ }
} }
return true; return true;
} }