From 03d1391ded7ac0702f3749f669bd34ee41bba597 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 6 Dec 2015 23:37:37 -0800 Subject: [PATCH] merge seq and string operators Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index fd370e425..96590a40a 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -139,7 +139,7 @@ br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) { std::string b; m_es.reset(); m_util.str.get_concat(a, m_es); - unsigned len = 0; + size_t len = 0; size_t j = 0; for (unsigned i = 0; i < m_es.size(); ++i) { if (m_util.str.is_string(m_es[i], b)) { @@ -151,7 +151,7 @@ br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) { } } if (j == 0) { - result = m_autil.mk_numeral(rational(b.length(), rational::ui64()), true); + result = m_autil.mk_numeral(rational(len, rational::ui64()), true); return BR_DONE; } if (j != m_es.size()) {