From 3eb849ad9e4a270ac0e2eddd01a7ba78f5b82df3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 9 Aug 2021 15:32:04 -0700 Subject: [PATCH] rewrite equality too Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 2 +- src/ast/seq_decl_plugin.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 1a3208d0f..12c0e560b 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1950,7 +1950,7 @@ br_status seq_rewriter::mk_seq_replace_all(expr* a, expr* b, expr* c, expr_ref& } if (a == b) { result = m().mk_ite(str().mk_is_empty(b), str().mk_empty(a->get_sort()), c); - return BR_REWRITE1; + return BR_REWRITE2; } zstring s1, s2; expr_ref_vector strs(m()); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 273eac2c5..82ab83681 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -1070,7 +1070,7 @@ std::ostream& seq_util::rex::pp::compact_helper_seq(std::ostream& out, expr* s) compact_helper_seq(out, e); } else if (re.u.str.is_string(s, z)) { - for (int i = 0; i < z.length(); i++) + for (unsigned i = 0; i < z.length(); i++) out << (char)z[i]; } //using braces to indicate 'full' output