diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
index 7818c373c..6b7bbea67 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
@@ -993,13 +993,7 @@ void bit_blaster_tpl<Cfg>::mk_ext_rotate_left_right(unsigned sz, expr * const *
         for (unsigned j = 0; j < sz; ++j)
             out_bits.push_back(a_bits[j]);
         expr_ref_vector out(m());
-        auto mk_ite = [&](expr* bit_i, expr* th, expr* el)  {
-            if (m().is_false(bit_i))
-                return el;
-            if (m().is_true(bit_i))
-                return th;
-            return (expr*)(m().mk_ite(bit_i, th, el));
-        };
+        expr_ref tmp(m());
         for (unsigned i = 0, p = 1; i < sz; ++i) {
             auto bit_i = b_bits[i];
             // rotate by p if bit_i is set.
@@ -1008,7 +1002,8 @@ void bit_blaster_tpl<Cfg>::mk_ext_rotate_left_right(unsigned sz, expr * const *
                 out.reset();
                 for (unsigned j = 0; j < sz; ++j) {
                     unsigned src = (Left ? (sz + j - p) : (j + p)) % sz;
-                    out.push_back(mk_ite(bit_i, out_bits.get(src), out_bits.get(j)));
+                    mk_ite(bit_i, out_bits.get(src), out_bits.get(j), tmp));
+                    out.push_back(tmp);
                 }
                 out_bits.reset();
                 out_bits.append(out);