From e14e3ef291218c720e844caa50487d7dd57ea230 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 22 May 2021 10:27:53 -0700 Subject: [PATCH] #5140 --- src/ast/rewriter/seq_rewriter.cpp | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 4f71fdfe7..8c0b72960 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -4884,13 +4884,17 @@ bool seq_rewriter::reduce_itos(expr_ref_vector& ls, expr_ref_vector& rs, str().is_itos(ls.get(0), n) && is_string(rs.size(), rs.data(), s)) { std::string s1 = s.encode(); - rational r(s1.c_str()); - if (s1 == r.to_string()) { - eqs.push_back(n, m_autil.mk_numeral(r, true)); - ls.reset(); - rs.reset(); - return true; + try { + rational r(s1.c_str()); + if (s1 == r.to_string()) { + eqs.push_back(n, m_autil.mk_numeral(r, true)); + ls.reset(); + rs.reset(); + return true; + } } + catch (...) + { } } return true; }