mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 20:31:21 +00:00
Code Activity

merge seq and string operators

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-06 23:37:37 -08:00
parent 8bb73c8eae
commit 03d1391ded
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -139,7 +139,7 @@ br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) {
std::string b; std::string b;
m_es.reset(); m_es.reset();
m_util.str.get_concat(a, m_es); m_util.str.get_concat(a, m_es);
unsigned len = 0; size_t len = 0;
size_t j = 0; size_t j = 0;
for (unsigned i = 0; i < m_es.size(); ++i) { for (unsigned i = 0; i < m_es.size(); ++i) {
if (m_util.str.is_string(m_es[i], b)) { 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) { 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; return BR_DONE;
} }
if (j != m_es.size()) { if (j != m_es.size()) {