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)));
 }