diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
index d603e9b07..6091567cb 100644
--- a/src/ast/rewriter/bool_rewriter.cpp
+++ b/src/ast/rewriter/bool_rewriter.cpp
@@ -19,6 +19,7 @@ Notes:
 #include "ast/rewriter/bool_rewriter.h"
 #include "params/bool_rewriter_params.hpp"
 #include "ast/rewriter/rewriter_def.h"
+#include "ast/rewriter/expr_safe_replace.h"
 #include "ast/ast_lt.h"
 #include "ast/for_each_expr.h"
 #include <algorithm>
@@ -1195,9 +1196,15 @@ bool bool_rewriter::decompose_ite(expr *r, expr_ref &c, expr_ref &th, expr_ref &
     }
     for (expr *e : subterms::ground(expr_ref(r, m()))) {
         if (m().is_ite(e, cond, r1, r2)) {
+            expr_safe_replace rep1(m());
+            expr_safe_replace rep2(m());
+            rep1.insert(cond, m().mk_true());
+            rep2.insert(cond, m().mk_false());
             c = cond;
             th = r1;
             el = r2;
+            rep1(th);
+            rep2(el);
             return true;
         }
     }
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 555f9523d..e7c72ed90 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -6130,7 +6130,7 @@ lbool seq_rewriter::some_string_in_re(expr_mark& visited, expr* r, unsigned_vect
             }
             if (has_bounds) {
 
-                if (any_of(subterms::all(th), [&](expr *t) { return m().is_ite(t); })) {
+                if (any_of(subterms::ground(th), [&](expr *t) { return m().is_ite(t); })) {
                     if (low > 0)
                         exclude.push_back({0, low - 1});
                     if (high < zstring::unicode_max_char())