diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 2b9d738c0..34290bf74 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -4832,26 +4832,32 @@ br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
         sort* srt = a->get_sort();
         bool has_left = (lo_v > 0);
         bool has_right = (hi_v < max_c);
+        auto empty_re = [&]() { return re().mk_empty(srt); };
+        auto full_re = [&]() { return re().mk_full_seq(srt); };
         if (!has_left && !has_right) {
             // [0, max_c]: complement is empty
-            result = re().mk_empty(srt);
+            result = empty_re();
+            return BR_DONE;
+        }
+        if (lo_v > hi_v) {
+            result = full_re();
             return BR_DONE;
         }
         if (!has_left) {
             // [0, b]: complement is [b+1, max]
-            result = re().mk_range(srt, hi_v + 1, max_c);
-            return BR_REWRITE1;
+            result = re().mk_union(empty_re(), re().mk_concat(re().mk_range(srt, hi_v + 1, max_c), full_re()));
+            return BR_DONE;
         }
         if (!has_right) {
             // [a, max]: complement is [0, a-1]
-            result = re().mk_range(srt, 0u, lo_v - 1);
-            return BR_REWRITE1;
+            result = re().mk_union(empty_re(), re().mk_concat(re().mk_range(srt, 0u, lo_v - 1), full_re()));
+            return BR_DONE;
         }
         // General: [a, b] → [0, a-1] ∪ [b+1, max]
         auto left = re().mk_range(srt, 0u, lo_v - 1);
         auto right = re().mk_range(srt, hi_v + 1, max_c);
-        result = re().mk_union(left, right);
-        return BR_REWRITE1;
+        result = re().mk_union(empty_re(), re().mk_concat(re().mk_union(left, right), full_re()));
+        return BR_DONE;
     }
     return BR_FAILED;
 }
diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp
index 2b9f5ba51..d35da4679 100644
--- a/src/smt/theory_array.cpp
+++ b/src/smt/theory_array.cpp
@@ -396,15 +396,15 @@ namespace smt {
     }
 
     final_check_status theory_array::assert_delayed_axioms() {
-        if (!m_params.m_array_delay_exp_axiom)
-            return FC_DONE;
         final_check_status r = FC_DONE;
-        unsigned num_vars = get_num_vars();
-        for (unsigned v = 0; v < num_vars; ++v) {
-            var_data * d = m_var_data[v];
-            if (d->m_prop_upward && instantiate_axiom2b_for(v))
-                r = FC_CONTINUE;
-        }      
+        if (m_params.m_array_delay_exp_axiom) {
+            unsigned num_vars = get_num_vars();
+            for (unsigned v = 0; v < num_vars; ++v) {
+                var_data *d = m_var_data[v];
+                if (d->m_prop_upward && instantiate_axiom2b_for(v))
+                    r = FC_CONTINUE;
+            }
+        }
         return r;
     }
 
diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp
index 1bfa05584..428c13408 100644
--- a/src/smt/theory_array_base.cpp
+++ b/src/smt/theory_array_base.cpp
@@ -67,7 +67,6 @@ namespace smt {
         return mk_select(num_args, args);
     }
 
-
     app * theory_array_base::mk_store(unsigned num_args, expr * const * args) {
         return m.mk_app(get_family_id(), OP_STORE, 0, nullptr, num_args, args);
     }
@@ -279,7 +278,7 @@ namespace smt {
         SASSERT(n1->get_num_args() == n2->get_num_args());
         unsigned n = n1->get_num_args();
         // skipping first argument of the select.
-        for(unsigned i = 1; i < n; ++i) {
+        for (unsigned i = 1; i < n; ++i) {
             if (n1->get_arg(i)->get_root() != n2->get_arg(i)->get_root()) {
                 return false;
             }
@@ -295,9 +294,8 @@ namespace smt {
         enode * r1    = v1->get_root();
         enode * r2    = v2->get_root();
 
-        if (r1->get_class_size() > r2->get_class_size()) {
-            std::swap(r1, r2);
-        }
+        if (r1->get_class_size() > r2->get_class_size()) 
+            std::swap(r1, r2);        
 
         m_array_value.reset();
         // populate m_array_value if the select(a, i) parent terms of r1
@@ -335,7 +333,7 @@ namespace smt {
             return false; // axiom was already instantiated
         if (already_diseq(n1, n2))
             return false;
-        m_extensionality_todo.push_back(std::make_pair(n1, n2));         
+        m_extensionality_todo.push_back({n1, n2});         
         return true;
     }
 
@@ -348,7 +346,7 @@ namespace smt {
         enode * nodes[2] = { a1, a2 };
         if (!ctx.add_fingerprint(this, 1, 2, nodes))
             return; // axiom was already instantiated
-        m_congruent_todo.push_back(std::make_pair(a1, a2));         
+        m_congruent_todo.push_back({a1, a2});         
     }
 
    
@@ -581,11 +579,11 @@ namespace smt {
                 enode *    n2 = get_enode(v2);
                 sort *     s2 = n2->get_sort();
                 if (s1 == s2 && !ctx.is_diseq(n1, n2)) {
-                    app * eq  = mk_eq_atom(n1->get_expr(), n2->get_expr());
-                    if (!ctx.b_internalized(eq) || !ctx.is_relevant(eq)) {
+                    app_ref eq  = app_ref(mk_eq_atom(n1->get_expr(), n2->get_expr()), m);
+                    if (!ctx.b_internalized(eq.get()) || !ctx.is_relevant(eq.get())) {
                         result++;
                         ctx.internalize(eq, true);
-                        ctx.mark_as_relevant(eq);
+                        ctx.mark_as_relevant(eq.get());
                     }
                 }
             }
@@ -850,7 +848,7 @@ namespace smt {
                 if (i < num_args) {
                     SASSERT(!parent_sel_set->contains(sel) || (*(parent_sel_set->find(sel)))->get_root() == sel->get_root());
                     parent_sel_set->insert(sel);
-                    todo.push_back(std::make_pair(parent_root, sel));
+                    todo.push_back({parent_root, sel});
                 }
             }
         }