From 7bc3b4e3810c81dff9ad677cd3a1d63bced7ee63 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 22 Nov 2018 13:03:55 -0800 Subject: [PATCH] swap order in equality for emptiness check to deal with rewriter Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 4 ++-- src/ast/seq_decl_plugin.cpp | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 04ab51538..00debef6a 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1241,7 +1241,7 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { else { result = m().mk_eq(a, m_util.str.mk_concat(seq)); } - return BR_REWRITE_FULL; + return BR_REWRITE3; } if (!is_sequence(a, seq)) { @@ -1569,7 +1569,7 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) { return BR_FAILED; } for (unsigned i = 0; i < lhs.size(); ++i) { - res.push_back(m().mk_eq(lhs[i].get(), rhs[i].get())); + res.push_back(m().mk_eq(lhs.get(i), rhs.get(i))); } result = mk_and(res); return BR_REWRITE3; diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 4bcc664a4..98c79abe8 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -988,7 +988,7 @@ void seq_util::str::get_concat_units(expr* e, expr_ref_vector& es) const { } app* seq_util::str::mk_is_empty(expr* s) const { - return m.mk_eq(mk_empty(get_sort(s)), s); + return m.mk_eq(s, mk_empty(get_sort(s))); }