From 09aaadf9638073d09daf830aa877f2cea2787936 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <mt@debian.org>
Date: Wed, 22 Jul 2026 04:03:02 +0200
Subject: [PATCH] Sequence AST-creating arguments in rewriters for
 cross-compiler determinism (#10165)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

### Problem

The order of evaluation of function arguments is unspecified in C++
(arguments are indeterminately sequenced since C++17). Compilers use
this freedom differently:

```c++
static int f(int i) { printf("%d ", i); return i; }
static void g(int, int, int) { printf("\n"); }
int main() { g(f(1), f(2), f(3)); }
```
| compiler/target | output |
|---|---|
| gcc 13, x86_64 | `3 2 1` |
| gcc 13, aarch64 | `1 2 3` |
| clang 18, x86_64 | `1 2 3` |

Z3 has many call sites where **two or more arguments each create AST
nodes**, e.g. (before this PR, `bv_rewriter.cpp:876`):

```c++
result = m.mk_ite(c, m_mk_extract(high, low, t), m_mk_extract(high, low, e));
```

The two extract nodes are hash-consed and receive their AST ids in
evaluation order, so the id assignment differs between
compilers/targets. AST ids feed heuristic tie-breaking throughout the
solver (`bool_rewriter`'s `m_order_eq` equality-operand ordering,
id-based sorts in `array_rewriter`, case-split ordering, ...), so
**byte-identical input takes different solver paths depending on the
compiler and architecture z3 was built with**.

### Evidence

Investigated while chasing cross-platform proof-time instability in
CBMC/mldsa-native CI (diffblue/cbmc#8991), on byte-identical ~12 MB SMT2
instances (bit-vectors + arrays + quantifiers), with the `string_hash`
fix from #10163 applied to isolate this effect. Z3 4.15.3, gcc 13 on
x86_64 Linux and aarch64 Linux (Graviton):

* one instance: **17 s on x86_64 vs 1633 s on aarch64** (both `unsat`; a
sibling instance shows the reverse direction). Run-to-run within one
host: ±1 %.
* Instrumenting `ast_manager::register_node_core` with an order
fingerprint (running hash over `(node hash, node id)`) shows both
architectures construct **identical AST sequences up to registration
#41,789**, where x86_64 creates `(extract[0:0] #xFFFFFFFF)` before
`(extract[0:0] #xFFFFFFFE)` and aarch64 the other way around — from
identical call stacks at the `mk_ite`-over-two-`mk_extract` site quoted
above. All divergence between the two hosts flows from such events
(pointer/ASLR effects experimentally excluded: fingerprints are
invariant under `setarch -R` and across repeated runs).
* Sequencing that one site by hand moved the first divergence to
#248,118 — the analogous `mk_ite(c, mk_select(...), mk_select(...))`
site in `array_rewriter.cpp`. Sequencing that one, too, moved it to
#248,411, inside `nnf::imp::process_iff_xor` — i.e. the next layer of
the same onion.
* With the whole `ast/rewriter` layer swept (this PR), the instrumented
builds produce **identical AST construction traces on both architectures
throughout the entire rewriter phase** of this 546k-line industrial
instance; the first divergence left is the NNF one.

### Fix

Following the precedent of 37904b9e8, e113d39aa, 360193098, 93ff8c76d,
9b88aaf13 ("parameter evaluation order", `bool_rewriter`/`seq_rewriter`)
and the existing comments in `seq_rewriter.cpp` ("introduce temporaries
to ensure deterministic evaluation order..."), this PR hoists
AST-creating arguments into named temporaries with a defined evaluation
order, across `src/ast/rewriter/` — 126 call sites in 17 files. The
transformation is purely sequencing: it selects one of the two valid C++
evaluation orders and makes it the same everywhere. (Temporaries are raw
pointers in rewriter-local scope, matching the precedent commits;
nothing can trigger GC between creation and consumption.)

The sites were found with a small AST-argument scanner (statement-level
call sites whose argument list contains ≥ 2 top-level arguments that
each contain an AST-creating call); I am happy to share/contribute the
script. Known remaining work, deliberately out of scope here to keep the
diff reviewable:

* 41 sites in `src/ast/rewriter/` that need manual treatment (inside
`if` conditions, ternaries, or multi-statement expressions) — list
available on request;
* `src/ast/normal_forms/nnf.cpp` (`process_iff_xor`, proven divergent by
the trace above), ~7 sites in `src/ast/simplifiers/`, ~3 in
`src/ast/converters/`, ~9 in `src/ast/`;
* other theory/solver layers (`src/smt/`, `src/sat/`, ...) — divergences
there only matter after search starts, where paths have usually already
split, but a full sweep would be needed for bit-reproducibility across
compilers.

Together with #10163, this is a step towards z3 builds whose behaviour
does not depend on the compiler or target architecture — which matters
for verification CI that runs identical proofs on heterogeneous
platforms and expects comparable runtimes.

---------

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 src/ast/ast.cpp                              |  13 +-
 src/ast/bv_decl_plugin.cpp                   |  23 +-
 src/ast/converters/expr_inverter.cpp         |  13 +-
 src/ast/rewriter/arith_rewriter.cpp          | 247 +++++++++++++------
 src/ast/rewriter/array_rewriter.cpp          |   6 +-
 src/ast/rewriter/bv2int_translator.cpp       |  47 +++-
 src/ast/rewriter/bv_rewriter.cpp             | 192 +++++++++-----
 src/ast/rewriter/enum2bv_rewriter.cpp        |  11 +-
 src/ast/rewriter/factor_rewriter.cpp         |  12 +-
 src/ast/rewriter/finite_set_axioms.cpp       |  27 +-
 src/ast/rewriter/finite_set_rewriter.cpp     |  18 +-
 src/ast/rewriter/fpa_rewriter.cpp            |  14 +-
 src/ast/rewriter/pb2bv_rewriter.cpp          |  12 +-
 src/ast/rewriter/quant_hoist.cpp             |  12 +-
 src/ast/rewriter/seq_axioms.cpp              |  89 +++++--
 src/ast/rewriter/seq_derive.cpp              |  64 +++--
 src/ast/rewriter/seq_eq_solver.cpp           |   4 +-
 src/ast/rewriter/seq_range_collapse.cpp      |   6 +-
 src/ast/rewriter/seq_rewriter.cpp            | 222 ++++++++++++-----
 src/ast/rewriter/seq_split.cpp               |  27 +-
 src/ast/rewriter/th_rewriter.cpp             |  45 ++--
 src/ast/simplifiers/eliminate_predicates.cpp |   6 +-
 src/ast/simplifiers/euf_completion.cpp       |  28 ++-
 src/ast/simplifiers/factor_simplifier.cpp    |  10 +-
 24 files changed, 836 insertions(+), 312 deletions(-)

diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index b0fa217d62..edc4009b06 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -2102,10 +2102,15 @@ expr* ast_manager::coerce_to(expr* e, sort* s) {
     }
     if (s != se && s->get_family_id() == arith_family_id && is_bool(e)) {
         arith_util au(*this);
-        if (s->get_decl_kind() == REAL_SORT) 
-            return mk_ite(e, au.mk_real(1), au.mk_real(0));
-        else 
-            return mk_ite(e, au.mk_int(1), au.mk_int(0));
+        if (s->get_decl_kind() == REAL_SORT) {
+            auto _seqr0 = au.mk_real(1);
+            auto _seqr1 = au.mk_real(0);
+            return mk_ite(e, _seqr0, _seqr1);
+        } else {
+            auto _seq2108_0 = au.mk_int(1);
+            auto _seq2108_1 = au.mk_int(0);
+            return mk_ite(e, _seq2108_0, _seq2108_1);
+        }
     }
     else {
         return e;
diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
index 74368ecec5..c8dafb2ae3 100644
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@@ -977,9 +977,11 @@ app* bv_util::mk_sbv2int_as_ubv2int(expr* e) {
     arith_util autil(m_manager);
     unsigned sz = get_bv_size(e);
     expr_ref zero(mk_numeral(rational::zero(), sz), m_manager);
-    r = m_manager.mk_ite(mk_slt(e, zero),
-        autil.mk_sub(r, autil.mk_numeral(rational::power_of_two(sz), true)),
-        r);
+    {
+        auto _seq980_0 = mk_slt(e, zero);
+        auto _seq980_1 = autil.mk_sub(r, autil.mk_numeral(rational::power_of_two(sz), true));
+        r = m_manager.mk_ite(_seq980_0, _seq980_1, r);
+    }
     return r;
 }
 
@@ -1012,12 +1014,17 @@ void bv_util::mk_bv_divrem_bound(expr* t, expr_ref_vector& clause) {
     // OP_ULT is not handled by theory_bv::internalize_atom and would trigger UNREACHABLE.
     if (is_bv_urem(t) || is_bv_uremi(t))
         bound = m_manager.mk_not(mk_ule(b, t));
-    else if (is_bv_srem(t) || is_bv_sremi(t) || is_bv_smod(t) || is_bv_smodi(t))
-        bound = m_manager.mk_not(mk_ule(mk_abs(b), mk_abs(t)));
-    else if (is_bv_udiv(t) || is_bv_udivi(t))
+    else if (is_bv_srem(t) || is_bv_sremi(t) || is_bv_smod(t) || is_bv_smodi(t)) {
+        auto _seq0 = mk_abs(b);
+        auto _seq1 = mk_abs(t);
+        bound = m_manager.mk_not(mk_ule(_seq0, _seq1));
+    } else if (is_bv_udiv(t) || is_bv_udivi(t))
         bound = mk_ule(t, a);
-    else if (is_bv_sdiv(t) || is_bv_sdivi(t))
-        bound = mk_ule(mk_abs(t), mk_abs(a));
+    else if (is_bv_sdiv(t) || is_bv_sdivi(t)) {
+        auto _seq0 = mk_abs(t);
+        auto _seq1 = mk_abs(a);
+        bound = mk_ule(_seq0, _seq1);
+    }
     if (!bound)
         return;
     // clause encodes  b != 0 => bound  as the disjunction  (b = 0) \/ bound
diff --git a/src/ast/converters/expr_inverter.cpp b/src/ast/converters/expr_inverter.cpp
index 0e756ebe65..65b5ea16cf 100644
--- a/src/ast/converters/expr_inverter.cpp
+++ b/src/ast/converters/expr_inverter.cpp
@@ -337,8 +337,11 @@ class bv_expr_inverter : public iexpr_inverter {
                 ++sh;
             }
             mk_fresh_uncnstr_var_for(f, r);
-            if (sh > 0)
-                r = bv.mk_concat(bv.mk_extract(sz - sh - 1, 0, r), bv.mk_zero(sh));
+            if (sh > 0) {
+                auto _seq0 = bv.mk_extract(sz - sh - 1, 0, r);
+                auto _seq1 = bv.mk_zero(sh);
+                r = bv.mk_concat(_seq0, _seq1);
+            }
 
             if (m_mc) {
                 rational inv_r;
@@ -427,7 +430,11 @@ class bv_expr_inverter : public iexpr_inverter {
         if (uncnstr(arg1) && uncnstr(arg2)) {
             mk_fresh_uncnstr_var_for(f, r);
             if (m_mc) {
-                add_def(arg1, m.mk_ite(r, bv.mk_zero(bv_sz), bv.mk_one(bv_sz)));
+                {
+                    auto _seq430_0 = bv.mk_zero(bv_sz);
+                    auto _seq430_1 = bv.mk_one(bv_sz);
+                    add_def(arg1, m.mk_ite(r, _seq430_0, _seq430_1));
+                }
                 add_def(arg2, bv.mk_zero(bv_sz));
             }
             return true;
diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index b22ce62738..d002158800 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -662,16 +662,26 @@ br_status arith_rewriter::factor_le_ge_eq(expr * arg1, expr * arg2, op_kind kind
         expr* f = *opt_f;
         expr_ref f2 = remove_factor(f, arg1);
         expr* z = m_util.mk_numeral(rational(0), m_util.is_int(arg1));
-        result = m.mk_or(m_util.mk_eq(f, z), m_util.mk_eq(f2, z));
+        {
+            auto _seq665_0 = m_util.mk_eq(f, z);
+            auto _seq665_1 = m_util.mk_eq(f2, z);
+            result = m.mk_or(_seq665_0, _seq665_1);
+        }
         switch (kind) {
         case EQ: 
             break;
-        case GE:
-            result = m.mk_or(m.mk_iff(m_util.mk_ge(f, z), m_util.mk_ge(f2, z)), result);
+        case GE: {
+            auto _seq0 = m_util.mk_ge(f, z);
+            auto _seq1 = m_util.mk_ge(f2, z);
+            result = m.mk_or(m.mk_iff(_seq0, _seq1), result);
             break;
-        case LE:
-            result = m.mk_or(m.mk_not(m.mk_iff(m_util.mk_ge(f, z), m_util.mk_ge(f2, z))), result);
-            break;            
+        }
+        case LE: {
+            auto _seq0 = m_util.mk_ge(f, z);
+            auto _seq1 = m_util.mk_ge(f2, z);
+            result = m.mk_or(m.mk_not(m.mk_iff(_seq0, _seq1)), result);
+            break;
+        }
         }
         return BR_REWRITE3;                    
     }
@@ -859,7 +869,11 @@ bool arith_rewriter::is_arith_term(expr * n) const {
 br_status arith_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) {
     br_status st = BR_FAILED;
     if (m_eq2ineq) {
-        result = m.mk_and(m_util.mk_le(arg1, arg2), m_util.mk_ge(arg1, arg2));
+        {
+            auto _seq862_0 = m_util.mk_le(arg1, arg2);
+            auto _seq862_1 = m_util.mk_ge(arg1, arg2);
+            result = m.mk_and(_seq862_0, _seq862_1);
+        }
         st = BR_REWRITE2;
     }
     else if (m_arith_lhs || is_arith_term(arg1) || is_arith_term(arg2)) {
@@ -908,8 +922,11 @@ bool arith_rewriter::mk_eq_mod(expr* arg1, expr* arg2, expr_ref& result) {
         rational g = gcd(p, k, a, b);
         if (g == 1) {
             expr_ref nb(m_util.mk_numeral(b, true), m);
-            result = m.mk_eq(m_util.mk_mod(u, y),
-                             m_util.mk_mod(m_util.mk_mul(nb, arg2), y));
+            {
+                auto _seq911_0 = m_util.mk_mod(u, y);
+                auto _seq911_1 = m_util.mk_mod(m_util.mk_mul(nb, arg2), y);
+                result = m.mk_eq(_seq911_0, _seq911_1);
+            }
             return true;            
         }
     }
@@ -1229,10 +1246,17 @@ br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & resul
         TRACE(div_bug, tout << "v1: " << v1 << ", v2: " << v2 << "\n";);
         if (!v1.is_one() || !v2.is_one()) {
             v1 /= v2;
-            result = m_util.mk_mul(m_util.mk_numeral(v1, false),
-                                   m_util.mk_div(b, d));
+            {
+                auto _seq1232_0 = m_util.mk_numeral(v1, false);
+                auto _seq1232_1 = m_util.mk_div(b, d);
+                result = m_util.mk_mul(_seq1232_0, _seq1232_1);
+            }
             expr_ref z(m_util.mk_real(0), m);
-            result = m.mk_ite(m.mk_eq(d, z), m_util.mk_div(arg1, z), result);
+            {
+                auto _seq1235_0 = m.mk_eq(d, z);
+                auto _seq1235_1 = m_util.mk_div(arg1, z);
+                result = m.mk_ite(_seq1235_0, _seq1235_1, result);
+            }
             return BR_REWRITE2;
         }
     }
@@ -1242,7 +1266,11 @@ br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & resul
 }
 
 br_status arith_rewriter::mk_idivides(unsigned k, expr * arg, expr_ref & result) {
-    result = m.mk_eq(m_util.mk_mod(arg, m_util.mk_int(k)), m_util.mk_int(0));
+    {
+        auto _seq1245_0 = m_util.mk_mod(arg, m_util.mk_int(k));
+        auto _seq1245_1 = m_util.mk_int(0);
+        result = m.mk_eq(_seq1245_0, _seq1245_1);
+    }
     return BR_REWRITE2;
 }
 
@@ -1267,9 +1295,14 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
     if (is_num2 && v2.is_zero()) { 
         return BR_FAILED; 
     } 
-    if (arg1 == arg2) { 
-        expr_ref zero(m_util.mk_int(0), m); 
-        result = m.mk_ite(m.mk_eq(arg1, zero), m_util.mk_idiv(zero, zero), m_util.mk_int(1)); 
+    if (arg1 == arg2) {
+        expr_ref zero(m_util.mk_int(0), m);
+        {
+            auto _seq1272_0 = m.mk_eq(arg1, zero);
+            auto _seq1272_1 = m_util.mk_idiv(zero, zero);
+            auto _seq1272_2 = m_util.mk_int(1);
+            result = m.mk_ite(_seq1272_0, _seq1272_1, _seq1272_2);
+        }
         return BR_REWRITE3; 
     } 
     if (is_num2 && v2.is_pos() && m_util.is_add(arg1)) { 
@@ -1294,9 +1327,13 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
             return BR_REWRITE3;
         }
     } 
-    if (get_divides(arg1, arg2, result)) { 
-        expr_ref zero(m_util.mk_int(0), m); 
-        result = m.mk_ite(m.mk_eq(zero, arg2), m_util.mk_idiv(arg1, zero), result);
+    if (get_divides(arg1, arg2, result)) {
+        expr_ref zero(m_util.mk_int(0), m);
+        {
+            auto _seq1299_0 = m.mk_eq(zero, arg2);
+            auto _seq1299_1 = m_util.mk_idiv(arg1, zero);
+            result = m.mk_ite(_seq1299_0, _seq1299_1, result);
+        }
         return BR_REWRITE_FULL; 
     }
 #if 0
@@ -1366,13 +1403,13 @@ expr_ref arith_rewriter::remove_divisor(expr* arg, expr* num, expr* den) {
     num = args1.empty() ? m_util.mk_int(1) : m_util.mk_mul(args1.size(), args1.data()); 
     den = args2.empty() ? m_util.mk_int(1) : m_util.mk_mul(args2.size(), args2.data()); 
     expr_ref d(m_util.mk_idiv(num, den), m);
-    expr_ref nd(m_util.mk_idiv(m_util.mk_uminus(num), m_util.mk_uminus(den)), m);
-    return expr_ref(m.mk_ite(m.mk_eq(zero, arg), 
-                               m_util.mk_idiv(zero, zero), 
-                               m.mk_ite(m_util.mk_ge(arg, zero), 
-                                          d,
-                                          nd)),
-                    m);
+    auto _sequm0 = m_util.mk_uminus(num);
+    auto _sequm1 = m_util.mk_uminus(den);
+    expr_ref nd(m_util.mk_idiv(_sequm0, _sequm1), m);
+    auto _seqi0 = m.mk_eq(zero, arg);
+    auto _seqi1 = m_util.mk_idiv(zero, zero);
+    auto _seqi2 = m.mk_ite(m_util.mk_ge(arg, zero), d, nd);
+    return expr_ref(m.mk_ite(_seqi0, _seqi1, _seqi2), m);
 } 
  
 void arith_rewriter::flat_mul(expr* e, ptr_buffer<expr>& args) { 
@@ -1424,7 +1461,11 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
 
     if (arg1 == arg2 && !is_num2) {
         expr_ref zero(m_util.mk_int(0), m);
-        result = m.mk_ite(m.mk_eq(arg2, zero), m_util.mk_mod(zero, zero), zero);
+        {
+            auto _seq1427_0 = m.mk_eq(arg2, zero);
+            auto _seq1427_1 = m_util.mk_mod(zero, zero);
+            result = m.mk_ite(_seq1427_0, _seq1427_1, zero);
+        }
         return BR_DONE;
     }
 
@@ -1440,9 +1481,11 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
         // for y = 0, both sides evaluate to mod0(mod0(x,0),0).
         if (!is_num2 && m_util.is_int(arg2)) {
             expr_ref zero(m_util.mk_int(0), m);
-            result = m.mk_ite(m.mk_eq(arg2, zero),
-                              m_util.mk_mod(m_util.mk_mod(t1, zero), zero),
-                              arg1);
+            {
+                auto _seq1443_0 = m.mk_eq(arg2, zero);
+                auto _seq1443_1 = m_util.mk_mod(m_util.mk_mod(t1, zero), zero);
+                result = m.mk_ite(_seq1443_0, _seq1443_1, arg1);
+            }
             return BR_REWRITE2;
         }
     }
@@ -1517,7 +1560,11 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
 
     expr* x = nullptr, * y = nullptr, * z = nullptr;
     if (is_num2 && v2.is_pos() && m_util.is_mul(arg1, x, y) && m_util.is_numeral(x, v1, is_int) && v1 > 0 && divides(v1, v2)) {
-        result = m_util.mk_mul(m_util.mk_int(v1), m_util.mk_mod(y, m_util.mk_int(v2/v1)));        
+        {
+            auto _seq1520_0 = m_util.mk_int(v1);
+            auto _seq1520_1 = m_util.mk_mod(y, m_util.mk_int(v2 / v1));
+            result = m_util.mk_mul(_seq1520_0, _seq1520_1);
+        }
         return BR_REWRITE1;
     }
 
@@ -1594,9 +1641,11 @@ br_status arith_rewriter::mk_rem_core(expr * arg1, expr * arg2, expr_ref & resul
     }
     else if (m_elim_rem) {
         expr * mod = m_util.mk_mod(arg1, arg2);
-        result = m.mk_ite(m_util.mk_ge(arg2, m_util.mk_numeral(rational(0), true)),
-                            mod,
-                            m_util.mk_uminus(mod));
+        {
+            auto _seq1597_0 = m_util.mk_ge(arg2, m_util.mk_numeral(rational(0), true));
+            auto _seq1597_1 = m_util.mk_uminus(mod);
+            result = m.mk_ite(_seq1597_0, mod, _seq1597_1);
+        }
         TRACE(elim_rem, tout << "result: " << mk_ismt2_pp(result, m) << "\n";);
         return BR_REWRITE3;
     }
@@ -1639,8 +1688,11 @@ br_status arith_rewriter::mk_shl_core(unsigned sz, expr* arg1, expr* arg2, expr_
     if (is_num_y) {
         if (y >= sz) 
             result = m_util.mk_int(0);
-        else 
-            result = m_util.mk_mod(m_util.mk_mul(arg1, m_util.mk_int(rational::power_of_two(y.get_unsigned()))), m_util.mk_int(N));
+        else {
+            auto _seq1643_0 = m_util.mk_mul(arg1, m_util.mk_int(rational::power_of_two(y.get_unsigned())));
+            auto _seq1643_1 = m_util.mk_int(N);
+            result = m_util.mk_mod(_seq1643_0, _seq1643_1);
+        }
         return BR_REWRITE1;
     }
     if (is_num_x && x == 0) {
@@ -1809,26 +1861,35 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
 
     if (is_num_y && y.is_minus_one()) {        
         result = m_util.mk_div(m_util.mk_real(1), ensure_real(arg1));
-        result = m.mk_ite(m.mk_eq(arg1, m_util.mk_numeral(rational(0), m_util.is_int(arg1))),
-                            m_util.mk_real(0),
-                            result);        
+        {
+            auto _seq1812_0 = m.mk_eq(arg1, m_util.mk_numeral(rational(0), m_util.is_int(arg1)));
+            auto _seq1812_1 = m_util.mk_real(0);
+            result = m.mk_ite(_seq1812_0, _seq1812_1, result);
+        }
         return BR_REWRITE2;
     }
 
     if (is_num_y && y.is_neg()) {
-        // (^ t -k) --> (^ (/ 1 t) k)
-        result = m_util.mk_power(m_util.mk_div(m_util.mk_numeral(rational(1), false), arg1),
-                                 m_util.mk_numeral(-y, false));
-        result = m.mk_ite(m.mk_eq(arg1, m_util.mk_numeral(rational(0), m_util.is_int(arg1))),
-                            m_util.mk_real(0),
-                            result);
+        {
+            auto _seq1820_0 = m_util.mk_div(m_util.mk_numeral(rational(1), false), arg1);
+            auto _seq1820_1 = m_util.mk_numeral(-y, false);
+            result = m_util.mk_power(_seq1820_0, _seq1820_1);
+        }
+        {
+            auto _seq1822_0 = m.mk_eq(arg1, m_util.mk_numeral(rational(0), m_util.is_int(arg1)));
+            auto _seq1822_1 = m_util.mk_real(0);
+            result = m.mk_ite(_seq1822_0, _seq1822_1, result);
+        }
         return BR_REWRITE3;
     }
 
     if (is_num_y && !y.is_int() && !numerator(y).is_one()) {
-        // (^ t (/ p q)) --> (^ (^ t (/ 1 q)) p)
-        result = m_util.mk_power(m_util.mk_power(ensure_real(arg1), m_util.mk_numeral(rational(1)/denominator(y), false)),
-                                 m_util.mk_numeral(numerator(y), false));
+        {
+            auto _seq1830_0 =
+                m_util.mk_power(ensure_real(arg1), m_util.mk_numeral(rational(1) / denominator(y), false));
+            auto _seq1830_1 = m_util.mk_numeral(numerator(y), false);
+            result = m_util.mk_power(_seq1830_0, _seq1830_1);
+        }
         return BR_REWRITE3;
     }
 
@@ -2045,7 +2106,11 @@ br_status arith_rewriter::mk_is_int(expr * arg, expr_ref & result) {
 }
 
 br_status arith_rewriter::mk_abs_core(expr * arg, expr_ref & result) {
-    result = m.mk_ite(m_util.mk_ge(arg, m_util.mk_numeral(rational(0), m_util.is_int(arg))), arg, m_util.mk_uminus(arg));
+    {
+        auto _seq2048_0 = m_util.mk_ge(arg, m_util.mk_numeral(rational(0), m_util.is_int(arg)));
+        auto _seq2048_1 = m_util.mk_uminus(arg);
+        result = m.mk_ite(_seq2048_0, arg, _seq2048_1);
+    }
     return BR_REWRITE2;
 }
 
@@ -2138,7 +2203,9 @@ bool arith_rewriter::is_pi_integer_offset(expr * t, expr * & m) {
 }
 
 app * arith_rewriter::mk_sqrt(rational const & k) {
-    return m_util.mk_power(m_util.mk_numeral(k, false), m_util.mk_numeral(rational(1, 2), false));
+    auto _seq2141_0 = m_util.mk_numeral(k, false);
+    auto _seq2141_1 = m_util.mk_numeral(rational(1, 2), false);
+    return m_util.mk_power(_seq2141_0, _seq2141_1);
 }
 
 // Return a constant representing sin(k * pi).
@@ -2173,21 +2240,25 @@ expr * arith_rewriter::mk_sin_value(rational const & k) {
         return neg ? m_util.mk_uminus(result) : result;
     }
     if (k_prime == rational(1, 3) || k_prime == rational(2, 3)) {
-        // sin(pi/3)   == sin(2/3 pi) ==   Sqrt(3)/2
-        // sin(4/3 pi) == sin(5/3 pi) == - Sqrt(3)/2
-        expr * result = m_util.mk_div(mk_sqrt(rational(3)), m_util.mk_numeral(rational(2), false));
+        auto _seq2178_0 = mk_sqrt(rational(3));
+        auto _seq2178_1 = m_util.mk_numeral(rational(2), false);
+        expr* result = m_util.mk_div(_seq2178_0, _seq2178_1);
         return neg ? m_util.mk_uminus(result) : result;
     }
     if (k_prime == rational(1, 12) || k_prime == rational(11, 12)) {
-        // sin(1/12 pi)  == sin(11/12 pi)  ==  [sqrt(6) - sqrt(2)]/4
-        // sin(13/12 pi) == sin(23/12 pi)  == -[sqrt(6) - sqrt(2)]/4
-        expr * result = m_util.mk_div(m_util.mk_sub(mk_sqrt(rational(6)), mk_sqrt(rational(2))), m_util.mk_numeral(rational(4), false));
+        auto _seq2242_0 = mk_sqrt(rational(6));
+        auto _seq2242_1 = mk_sqrt(rational(2));
+        auto _seq2184_0 = m_util.mk_sub(_seq2242_0, _seq2242_1);
+        auto _seq2184_1 = m_util.mk_numeral(rational(4), false);
+        expr* result = m_util.mk_div(_seq2184_0, _seq2184_1);
         return neg ? m_util.mk_uminus(result) : result;
     }
     if (k_prime == rational(5, 12) || k_prime == rational(7, 12)) {
-        // sin(5/12 pi)  == sin(7/12 pi)   == [sqrt(6) + sqrt(2)]/4
-        // sin(17/12 pi) == sin(19/12 pi)  == -[sqrt(6) + sqrt(2)]/4
-        expr * result = m_util.mk_div(m_util.mk_add(mk_sqrt(rational(6)), mk_sqrt(rational(2))), m_util.mk_numeral(rational(4), false));
+        auto _seq2248_0 = mk_sqrt(rational(6));
+        auto _seq2248_1 = mk_sqrt(rational(2));
+        auto _seq2190_0 = m_util.mk_add(_seq2248_0, _seq2248_1);
+        auto _seq2190_1 = m_util.mk_numeral(rational(4), false);
+        expr* result = m_util.mk_div(_seq2190_0, _seq2190_1);
         return neg ? m_util.mk_uminus(result) : result;
     }
     return nullptr;
@@ -2201,8 +2272,13 @@ br_status arith_rewriter::mk_sin_core(expr * arg, expr_ref & result) {
         return BR_DONE;
     }
     if (m_util.is_acos(arg, x)) {
-        // sin(acos(x)) == sqrt(1 - x^2)
-        result = m_util.mk_power(m_util.mk_sub(m_util.mk_real(1), m_util.mk_mul(x,x)), m_util.mk_numeral(rational(1,2), false));
+        {
+            auto _seq2265_0 = m_util.mk_real(1);
+            auto _seq2265_1 = m_util.mk_mul(x, x);
+            auto _seq2205_0 = m_util.mk_sub(_seq2265_0, _seq2265_1);
+            auto _seq2205_1 = m_util.mk_numeral(rational(1, 2), false);
+            result = m_util.mk_power(_seq2205_0, _seq2205_1);
+        }
         return BR_REWRITE_FULL;
     }
     rational k;
@@ -2365,7 +2441,11 @@ br_status arith_rewriter::mk_tan_core(expr * arg, expr_ref & result) {
 
  end:
     if (m_expand_tan) {
-        result = m_util.mk_div(m_util.mk_sin(arg), m_util.mk_cos(arg));
+        {
+            auto _seq2368_0 = m_util.mk_sin(arg);
+            auto _seq2368_1 = m_util.mk_cos(arg);
+            result = m_util.mk_div(_seq2368_0, _seq2368_1);
+        }
         return BR_REWRITE2;
     }
     return BR_FAILED;
@@ -2401,14 +2481,18 @@ br_status arith_rewriter::mk_asin_core(expr * arg, expr_ref & result) {
         if (k.is_one()) {
             // asin(1)  == pi/2
             // asin(-1) == -pi/2
-            result = m_util.mk_mul(m_util.mk_numeral(rational(neg ? -1 : 1, 2), false), m_util.mk_pi());
+            auto _seqp0 = m_util.mk_numeral(rational(neg ? -1 : 1, 2), false);
+            auto _seqp1 = m_util.mk_pi();
+            result = m_util.mk_mul(_seqp0, _seqp1);
             return BR_REWRITE2;
         }
 
         if (k == rational(1, 2)) {
             // asin(1/2)  == pi/6
             // asin(-1/2) == -pi/6
-            result = m_util.mk_mul(m_util.mk_numeral(rational(neg ? -1 : 1, 6), false), m_util.mk_pi());
+            auto _seqp0 = m_util.mk_numeral(rational(neg ? -1 : 1, 6), false);
+            auto _seqp1 = m_util.mk_pi();
+            result = m_util.mk_mul(_seqp0, _seqp1);
             return BR_REWRITE2;
         }
     }
@@ -2428,8 +2512,11 @@ br_status arith_rewriter::mk_acos_core(expr * arg, expr_ref & result) {
     rational k;
     if (is_numeral(arg, k)) {
         if (k.is_zero()) {
-            // acos(0) = pi/2
-            result = m_util.mk_mul(m_util.mk_numeral(rational(1, 2), false), m_util.mk_pi());
+            {
+                auto _seq2432_0 = m_util.mk_numeral(rational(1, 2), false);
+                auto _seq2432_1 = m_util.mk_pi();
+                result = m_util.mk_mul(_seq2432_0, _seq2432_1);
+            }
             return BR_REWRITE2;
         }
         if (k.is_one()) {
@@ -2443,13 +2530,19 @@ br_status arith_rewriter::mk_acos_core(expr * arg, expr_ref & result) {
             return BR_DONE;
         }
         if (k == rational(1, 2)) {
-            // acos(1/2) = pi/3
-            result = m_util.mk_mul(m_util.mk_numeral(rational(1, 3), false), m_util.mk_pi());
+            {
+                auto _seq2447_0 = m_util.mk_numeral(rational(1, 3), false);
+                auto _seq2447_1 = m_util.mk_pi();
+                result = m_util.mk_mul(_seq2447_0, _seq2447_1);
+            }
             return BR_REWRITE2;
         }
         if (k == rational(-1, 2)) {
-            // acos(-1/2) = 2/3 pi
-            result = m_util.mk_mul(m_util.mk_numeral(rational(2, 3), false), m_util.mk_pi());
+            {
+                auto _seq2452_0 = m_util.mk_numeral(rational(2, 3), false);
+                auto _seq2452_1 = m_util.mk_pi();
+                result = m_util.mk_mul(_seq2452_0, _seq2452_1);
+            }
             return BR_REWRITE2;
         }
     }
@@ -2465,14 +2558,20 @@ br_status arith_rewriter::mk_atan_core(expr * arg, expr_ref & result) {
         }
 
         if (k.is_one()) {
-            // atan(1)  == pi/4
-            result = m_util.mk_mul(m_util.mk_numeral(rational(1, 4), false), m_util.mk_pi());
+            {
+                auto _seq2469_0 = m_util.mk_numeral(rational(1, 4), false);
+                auto _seq2469_1 = m_util.mk_pi();
+                result = m_util.mk_mul(_seq2469_0, _seq2469_1);
+            }
             return BR_REWRITE2;
         }
 
         if (k.is_minus_one()) {
-            // atan(-1) == -pi/4
-            result = m_util.mk_mul(m_util.mk_numeral(rational(-1, 4), false), m_util.mk_pi());
+            {
+                auto _seq2475_0 = m_util.mk_numeral(rational(-1, 4), false);
+                auto _seq2475_1 = m_util.mk_pi();
+                result = m_util.mk_mul(_seq2475_0, _seq2475_1);
+            }
             return BR_REWRITE2;
         }
 
diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp
index 5bad27defe..8947bae759 100644
--- a/src/ast/rewriter/array_rewriter.cpp
+++ b/src/ast/rewriter/array_rewriter.cpp
@@ -392,7 +392,11 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args,
         args1.append(num_args-1, args + 1);
         args2.push_back(el);
         args2.append(num_args-1, args + 1);
-        result = m().mk_ite(c, m_util.mk_select(num_args, args1.data()), m_util.mk_select(num_args, args2.data()));
+        {
+            auto _seq395_0 = m_util.mk_select(num_args, args1.data());
+            auto _seq395_1 = m_util.mk_select(num_args, args2.data());
+            result = m().mk_ite(c, _seq395_0, _seq395_1);
+        }
         return BR_REWRITE2;
     }
     
diff --git a/src/ast/rewriter/bv2int_translator.cpp b/src/ast/rewriter/bv2int_translator.cpp
index 042e018558..b8696923c0 100644
--- a/src/ast/rewriter/bv2int_translator.cpp
+++ b/src/ast/rewriter/bv2int_translator.cpp
@@ -188,7 +188,9 @@ expr_ref bv2int_translator::mk_le(expr* x, expr* y) {
         return expr_ref(a.mk_le(x, y), m);
     if (a.is_numeral(x))
         return expr_ref(a.mk_ge(y, x), m);
-    return expr_ref(a.mk_le(a.mk_sub(x, y), a.mk_numeral(rational(0), x->get_sort())), m);
+    auto _seq0 = a.mk_sub(x, y);
+    auto _seq1 = a.mk_numeral(rational(0), x->get_sort());
+    return expr_ref(a.mk_le(_seq0, _seq1), m);
 }
 
 expr_ref bv2int_translator::mk_lt(expr* x, expr* y) {
@@ -364,7 +366,11 @@ void bv2int_translator::translate_bv(app* e) {
             rational N = bv_size(e);
             expr* x = umod(e, 0), * y = umod(e, 1);
             expr* signx = a.mk_ge(x, a.mk_int(N / 2));
-            r = m.mk_ite(signx, a.mk_int(-1), a.mk_int(0));
+            {
+                auto _seq367_0 = a.mk_int(-1);
+                auto _seq367_1 = a.mk_int(0);
+                r = m.mk_ite(signx, _seq367_0, _seq367_1);
+            }
             IF_VERBOSE(4, verbose_stream() << "ashr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
             for (unsigned i = 0; i < sz; ++i) {
                 expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i)));
@@ -431,7 +437,12 @@ void bv2int_translator::translate_bv(app* e) {
         break;
     case OP_BCOMP:
         bv_expr = e->get_arg(0);
-        r = m.mk_ite(m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(1), a.mk_int(0));
+        {
+            auto _seq434_0 = m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1));
+            auto _seq434_1 = a.mk_int(1);
+            auto _seq434_2 = a.mk_int(0);
+            r = m.mk_ite(_seq434_0, _seq434_1, _seq434_2);
+        }
         break;
     case OP_BSMOD_I:
     case OP_BSMOD: {
@@ -448,8 +459,16 @@ void bv2int_translator::translate_bv(app* e) {
         // x >= 0, y >= 0 ->  u
         r = a.mk_uminus(u);
         r = m.mk_ite(m.mk_and(m.mk_not(signx), signy), add(u, y), r);
-        r = m.mk_ite(m.mk_and(signx, m.mk_not(signy)), a.mk_sub(y, u), r);
-        r = m.mk_ite(m.mk_and(m.mk_not(signx), m.mk_not(signy)), u, r);
+        {
+            auto _seq451_0 = m.mk_and(signx, m.mk_not(signy));
+            auto _seq451_1 = a.mk_sub(y, u);
+            r = m.mk_ite(_seq451_0, _seq451_1, r);
+        }
+        {
+            auto _seq0 = m.mk_not(signx);
+            auto _seq1 = m.mk_not(signy);
+            r = m.mk_ite(m.mk_and(_seq0, _seq1), u, r);
+        }
         r = if_eq(u, 0, a.mk_int(0), r);
         r = if_eq(y, 0, x, r);
         break;
@@ -471,8 +490,16 @@ void bv2int_translator::translate_bv(app* e) {
         x = m.mk_ite(signx, a.mk_sub(a.mk_int(N), x), x);
         y = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y);
         expr* d = a.mk_idiv(x, y);
-        r = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d));
-        r = if_eq(y, 0, m.mk_ite(signx, a.mk_int(1), a.mk_int(-1)), r);
+        {
+            auto _seq474_0 = m.mk_iff(signx, signy);
+            auto _seq474_1 = a.mk_uminus(d);
+            r = m.mk_ite(_seq474_0, d, _seq474_1);
+        }
+        {
+            auto _seq0 = a.mk_int(1);
+            auto _seq1 = a.mk_int(-1);
+            r = if_eq(y, 0, m.mk_ite(signx, _seq0, _seq1), r);
+        }
         break;
     }
     case OP_BSREM_I:
@@ -486,7 +513,11 @@ void bv2int_translator::translate_bv(app* e) {
         expr* absx = m.mk_ite(signx, a.mk_sub(a.mk_int(N), x), x);
         expr* absy = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y);
         expr* d = a.mk_idiv(absx, absy);
-        d = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d));
+        {
+            auto _seq489_0 = m.mk_iff(signx, signy);
+            auto _seq489_1 = a.mk_uminus(d);
+            d = m.mk_ite(_seq489_0, d, _seq489_1);
+        }
         r = a.mk_sub(x, mul(d, y));
         r = if_eq(y, 0, x, r);
         break;
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index b2ae76dd78..0181b3fa20 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -383,8 +383,11 @@ br_status bv_rewriter::rw_leq_overflow(bool is_signed, expr * a, expr * b, expr_
     }
     else {
         SASSERT(lower.is_pos());
-        result = m.mk_and(m_util.mk_ule(mk_numeral(lower, sz), common),
-                            m_util.mk_ule(common, mk_numeral(upper, sz)));
+        {
+            auto _seq386_0 = m_util.mk_ule(mk_numeral(lower, sz), common);
+            auto _seq386_1 = m_util.mk_ule(common, mk_numeral(upper, sz));
+            result = m.mk_and(_seq386_0, _seq386_1);
+        }
     }
     return BR_REWRITE2;
 }
@@ -593,8 +596,11 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
         expr * b_2 = to_app(b)->get_arg(1);
         unsigned sz1 = get_bv_size(b_1);
         unsigned sz2 = get_bv_size(b_2);
-        result = m.mk_and(m.mk_eq(m_mk_extract(sz2+sz1-1, sz2, a), b_1),
-                            m_util.mk_ule(m_mk_extract(sz2-1, 0, a), b_2));
+        {
+            auto _seq596_0 = m.mk_eq(m_mk_extract(sz2+sz1-1, sz2, a), b_1);
+            auto _seq596_1 = m_util.mk_ule(m_mk_extract(sz2-1, 0, a), b_2);
+            result = m.mk_and(_seq596_0, _seq596_1);
+        }
         return BR_REWRITE3;
     }
 #else
@@ -869,7 +875,11 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_
     expr* c = nullptr, *t = nullptr, *e = nullptr;
     if (m.is_ite(arg, c, t, e) &&
         (t->get_ref_count() == 1 || e->get_ref_count() == 1 || !m.is_ite(t) || !m.is_ite(e))) {
-        result = m.mk_ite(c, m_mk_extract(high, low, t), m_mk_extract(high, low, e));
+        {
+            auto _seq872_0 = m_mk_extract(high, low, t);
+            auto _seq872_1 = m_mk_extract(high, low, e);
+            result = m.mk_ite(c, _seq872_0, _seq872_1);
+        }
         return BR_REWRITE2;
     }
 
@@ -932,9 +942,11 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) {
     if (m_util.is_bv_shl(arg1, x, y)) {
         expr_ref sum(m_util.mk_bv_add(y, arg2), m);
         expr_ref cond(m_util.mk_ule(y, sum), m);
-        result = m.mk_ite(cond, 
-                            m_util.mk_bv_shl(x, sum),
-                            mk_zero(bv_size));
+        {
+            auto _seq935_0 = m_util.mk_bv_shl(x, sum);
+            auto _seq935_1 = mk_zero(bv_size);
+            result = m.mk_ite(cond, _seq935_0, _seq935_1);
+        }
         return BR_REWRITE3;
     }
 
@@ -1078,7 +1090,11 @@ br_status bv_rewriter::mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result) {
         // (bvlshr x k) -> (concat bv0:k (extract [n-1:k] x))
 
         unsigned k = r2.get_unsigned();
-        result = m_util.mk_concat(mk_zero(k), m_mk_extract(bv_size - 1, k, arg1));
+        {
+            auto _seq1081_0 = mk_zero(k);
+            auto _seq1081_1 = m_mk_extract(bv_size - 1, k, arg1);
+            result = m_util.mk_concat(_seq1081_0, _seq1081_1);
+        }
         return BR_REWRITE2;
     }
 #if 0
@@ -1114,10 +1130,12 @@ br_status bv_rewriter::mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, e
                 return BR_REWRITE1;
             }
             else {
-                // The "hardware interpretation" for (bvsdiv x 0) is (ite (bvslt x #x0000) #x0001 #xffff)
-                result = m.mk_ite(m.mk_app(get_fid(), OP_SLT, arg1, mk_zero(bv_size)),
-                                    mk_one(bv_size),
-                                    mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size));
+                {
+                    auto _seq1118_0 = m.mk_app(get_fid(), OP_SLT, arg1, mk_zero(bv_size));
+                    auto _seq1118_1 = mk_one(bv_size);
+                    auto _seq1118_2 = mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size);
+                    result = m.mk_ite(_seq1118_0, _seq1118_1, _seq1118_2);
+                }
                 return BR_REWRITE2;
             }
         }
@@ -1143,9 +1161,12 @@ br_status bv_rewriter::mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, e
     }
 
     bv_size = get_bv_size(arg2);
-    result = m.mk_ite(m.mk_eq(arg2, mk_zero(bv_size)),
-                        m_util.mk_bv_sdiv0(arg1),
-                        m_util.mk_bv_sdiv_i(arg1, arg2));
+    {
+        auto _seq1146_0 = m.mk_eq(arg2, mk_zero(bv_size));
+        auto _seq1146_1 = m_util.mk_bv_sdiv0(arg1);
+        auto _seq1146_2 = m_util.mk_bv_sdiv_i(arg1, arg2);
+        result = m.mk_ite(_seq1146_0, _seq1146_1, _seq1146_2);
+    }
     return BR_REWRITE2;
 }
 
@@ -1198,9 +1219,12 @@ br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, e
     }
 
     bv_size = get_bv_size(arg2);
-    result = m.mk_ite(m.mk_eq(arg2, mk_zero(bv_size)),
-        m_util.mk_bv_udiv0(arg1),
-        m_util.mk_bv_udiv_i(arg1, arg2));
+    {
+        auto _seq1201_0 = m.mk_eq(arg2, mk_zero(bv_size));
+        auto _seq1201_1 = m_util.mk_bv_udiv0(arg1);
+        auto _seq1201_2 = m_util.mk_bv_udiv_i(arg1, arg2);
+        result = m.mk_ite(_seq1201_0, _seq1201_1, _seq1201_2);
+    }
 
     TRACE(bv_udiv, tout << mk_pp(arg1, m) << "\n" << mk_pp(arg2, m) << "\n---->\n" << mk_pp(result, m) << "\n";);
     return BR_REWRITE2;
@@ -1245,9 +1269,12 @@ br_status bv_rewriter::mk_bv_srem_core(expr * arg1, expr * arg2, bool hi_div0, e
     }
 
     bv_size = get_bv_size(arg2);
-    result = m.mk_ite(m.mk_eq(arg2, mk_zero(bv_size)),
-                        m.mk_app(get_fid(), OP_BSREM0, arg1),
-                        m.mk_app(get_fid(), OP_BSREM_I, arg1, arg2));
+    {
+        auto _seq1248_0 = m.mk_eq(arg2, mk_zero(bv_size));
+        auto _seq1248_1 = m.mk_app(get_fid(), OP_BSREM0, arg1);
+        auto _seq1248_2 = m.mk_app(get_fid(), OP_BSREM_I, arg1, arg2);
+        result = m.mk_ite(_seq1248_0, _seq1248_1, _seq1248_2);
+    }
     return BR_REWRITE2;
 }
 
@@ -1335,9 +1362,11 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e
         // urem(0, x) ==> ite(x = 0, urem0(x), 0)
         if (is_num1 && r1.is_zero()) {
             expr * zero = arg1;
-            result = m.mk_ite(m.mk_eq(arg2, zero),
-                                m_util.mk_bv_urem0(zero),
-                                zero);
+            {
+                auto _seq1338_0 = m.mk_eq(arg2, zero);
+                auto _seq1338_1 = m_util.mk_bv_urem0(zero);
+                result = m.mk_ite(_seq1338_0, _seq1338_1, zero);
+            }
             return BR_REWRITE2;
         }
 
@@ -1347,9 +1376,11 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e
             bv_size = get_bv_size(arg1);
             expr * x_minus_1 = arg1;
             expr * minus_one = mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size);
-            result = m.mk_ite(m.mk_eq(x, mk_zero(bv_size)),
-                                m_util.mk_bv_urem0(minus_one),
-                                x_minus_1);
+            {
+                auto _seq1350_0 = m.mk_eq(x, mk_zero(bv_size));
+                auto _seq1350_1 = m_util.mk_bv_urem0(minus_one);
+                result = m.mk_ite(_seq1350_0, _seq1350_1, x_minus_1);
+            }
             return BR_REWRITE2;
         }
     }
@@ -1377,9 +1408,12 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e
     }
 
     bv_size = get_bv_size(arg2);
-    result = m.mk_ite(m.mk_eq(arg2, mk_zero(bv_size)),
-                        m_util.mk_bv_urem0(arg1),
-                        m_util.mk_bv_urem_i(arg1, arg2));
+    {
+        auto _seq1380_0 = m.mk_eq(arg2, mk_zero(bv_size));
+        auto _seq1380_1 = m_util.mk_bv_urem0(arg1);
+        auto _seq1380_2 = m_util.mk_bv_urem_i(arg1, arg2);
+        result = m.mk_ite(_seq1380_0, _seq1380_1, _seq1380_2);
+    }
     return BR_REWRITE2;
 }
 
@@ -1441,8 +1475,16 @@ br_status bv_rewriter::mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, e
             unsigned nb = r2.get_num_bits();
             expr_ref a1(m_util.mk_bv_smod(a, arg2), m);
             expr_ref a2(m_util.mk_bv_smod(b, arg2), m);
-            a1 = m_util.mk_concat( mk_zero(bv_size - nb), m_mk_extract(nb-1,0,a1));
-            a2 = m_util.mk_concat( mk_zero(bv_size - nb), m_mk_extract(nb-1,0,a2));
+            {
+                auto _seq1444_0 = mk_zero(bv_size - nb);
+                auto _seq1444_1 = m_mk_extract(nb-1,0,a1);
+                a1 = m_util.mk_concat(_seq1444_0, _seq1444_1);
+            }
+            {
+                auto _seq1445_0 = mk_zero(bv_size - nb);
+                auto _seq1445_1 = m_mk_extract(nb-1,0,a2);
+                a2 = m_util.mk_concat(_seq1445_0, _seq1445_1);
+            }
             result = m_util.mk_bv_mul(a1, a2);
             std::cout << result << "\n";
             result = m_util.mk_bv_smod(result, arg2);
@@ -1458,9 +1500,12 @@ br_status bv_rewriter::mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, e
     }
 
     bv_size = get_bv_size(arg2);
-    result = m.mk_ite(m.mk_eq(arg2, mk_zero(bv_size)),
-                        m.mk_app(get_fid(), OP_BSMOD0, arg1),
-                        m.mk_app(get_fid(), OP_BSMOD_I, arg1, arg2));
+    {
+        auto _seq1461_0 = m.mk_eq(arg2, mk_zero(bv_size));
+        auto _seq1461_1 = m.mk_app(get_fid(), OP_BSMOD0, arg1);
+        auto _seq1461_2 = m.mk_app(get_fid(), OP_BSMOD_I, arg1, arg2);
+        result = m.mk_ite(_seq1461_0, _seq1461_1, _seq1461_2);
+    }
     return BR_REWRITE2;
 }
 
@@ -1677,7 +1722,11 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re
                 ptr_buffer<expr> args1, args2;
                 for (unsigned i = 0; i < new_args.size(); ++i)
                     args1.push_back(y), args2.push_back(z);
-                result = m.mk_ite(x, m_util.mk_concat(args1), m_util.mk_concat(args2));
+                {
+                    auto _seq1680_0 = m_util.mk_concat(args1);
+                    auto _seq1680_1 = m_util.mk_concat(args2);
+                    result = m.mk_ite(x, _seq1680_0, _seq1680_1);
+                }
                 return BR_REWRITE2;
             }
         }
@@ -2152,13 +2201,21 @@ br_status bv_rewriter::mk_bv_not(expr * arg, expr_ref & result) {
     expr* x, *y, *z;
     if (m.is_ite(arg, x, y, z) && m_util.is_numeral(y, val, bv_size)) {
         val = bitwise_not(bv_size, val);
-        result = m.mk_ite(x, m_util.mk_numeral(val, bv_size), m_util.mk_bv_not(z));
+        {
+            auto _seq2155_0 = m_util.mk_numeral(val, bv_size);
+            auto _seq2155_1 = m_util.mk_bv_not(z);
+            result = m.mk_ite(x, _seq2155_0, _seq2155_1);
+        }
         return BR_REWRITE2;
     }
 
     if (m.is_ite(arg, x, y, z) && m_util.is_numeral(z, val, bv_size)) {
         val = bitwise_not(bv_size, val);
-        result = m.mk_ite(x, m_util.mk_bv_not(y), m_util.mk_numeral(val, bv_size));
+        {
+            auto _seq2161_0 = m_util.mk_bv_not(y);
+            auto _seq2161_1 = m_util.mk_numeral(val, bv_size);
+            result = m.mk_ite(x, _seq2161_0, _seq2161_1);
+        }
         return BR_REWRITE2;
     }
 
@@ -2325,9 +2382,12 @@ br_status bv_rewriter::mk_bv_comp(expr * arg1, expr * arg2, expr_ref & result) {
         return BR_DONE;
     }
 
-    result = m.mk_ite(m.mk_eq(arg1, arg2),
-                        mk_one(1),
-                        mk_zero(1));
+    {
+        auto _seq2328_0 = m.mk_eq(arg1, arg2);
+        auto _seq2328_1 = mk_one(1);
+        auto _seq2328_2 = mk_zero(1);
+        result = m.mk_ite(_seq2328_0, _seq2328_1, _seq2328_2);
+    }
     return BR_REWRITE2;
 }
 
@@ -2603,8 +2663,9 @@ br_status bv_rewriter::mk_blast_eq_value(expr * lhs, expr * rhs, expr_ref & resu
     ptr_buffer<expr> new_args;
     for (unsigned i = 0; i < sz; ++i) {
         bool bit0 = (v % two).is_zero();
-        new_args.push_back(m.mk_eq(m_mk_extract(i,i, lhs),
-                                     mk_numeral(bit0 ? 0 : 1, 1)));
+        auto _seq0 = m_mk_extract(i, i, lhs);
+        auto _seq1 = mk_numeral(bit0 ? 0 : 1, 1);
+        new_args.push_back(m.mk_eq(_seq0, _seq1));
         div(v, two, v);
     }
     result = m.mk_and(new_args);
@@ -2648,8 +2709,11 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) {
         unsigned rsz1 = sz1 - low1;
         unsigned rsz2 = sz2 - low2;
         if (rsz1 == rsz2) {
-            new_eqs.push_back(m.mk_eq(m_mk_extract(sz1 - 1, low1, arg1),
-                                      m_mk_extract(sz2 - 1, low2, arg2)));
+            {
+                auto _seq2651_0 = m_mk_extract(sz1 - 1, low1, arg1);
+                auto _seq2651_1 = m_mk_extract(sz2 - 1, low2, arg2);
+                new_eqs.push_back(m.mk_eq(_seq2651_0, _seq2651_1));
+            }
             low1 = 0;
             low2 = 0;
             --i1;
@@ -2657,15 +2721,21 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) {
             continue;
         }
         else if (rsz1 < rsz2) {
-            new_eqs.push_back(m.mk_eq(m_mk_extract(sz1  - 1, low1, arg1),
-                                      m_mk_extract(rsz1 + low2 - 1, low2, arg2)));
+            {
+                auto _seq2660_0 = m_mk_extract(sz1 - 1, low1, arg1);
+                auto _seq2660_1 = m_mk_extract(rsz1 + low2 - 1, low2, arg2);
+                new_eqs.push_back(m.mk_eq(_seq2660_0, _seq2660_1));
+            }
             low1  = 0;
             low2 += rsz1;
             --i1;
         }
         else {
-            new_eqs.push_back(m.mk_eq(m_mk_extract(rsz2 + low1 - 1, low1, arg1),
-                                      m_mk_extract(sz2  - 1, low2, arg2)));
+            {
+                auto _seq2667_0 = m_mk_extract(rsz2 + low1 - 1, low1, arg1);
+                auto _seq2667_1 = m_mk_extract(sz2 - 1, low2, arg2);
+                new_eqs.push_back(m.mk_eq(_seq2667_0, _seq2667_1));
+            }
             low1 += rsz2;
             low2  = 0;
             --i2;
@@ -2810,8 +2880,11 @@ br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) {
             }
         }
         if (found) {
-            result = m.mk_eq(m_util.mk_numeral(c2_inv_val*c_val, sz),
-                               m_util.mk_bv_mul(m_util.mk_numeral(c2_inv_val, sz), rhs));
+            {
+                auto _seq2813_0 = m_util.mk_numeral(c2_inv_val * c_val, sz);
+                auto _seq2813_1 = m_util.mk_bv_mul(m_util.mk_numeral(c2_inv_val, sz), rhs);
+                result = m.mk_eq(_seq2813_0, _seq2813_1);
+            }
             return BR_REWRITE3;
         }
     }
@@ -3102,10 +3175,11 @@ br_status bv_rewriter::mk_distinct(unsigned num_args, expr * const * args, expr_
 
 br_status bv_rewriter::mk_bvsmul_overflow(unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 2);
-    result = m.mk_or(
-            m.mk_not(m_util.mk_bvsmul_no_ovfl(args[0], args[1])),
-            m.mk_not(m_util.mk_bvsmul_no_udfl(args[0], args[1]))
-    );
+    {
+        auto _seq3105_0 = m.mk_not(m_util.mk_bvsmul_no_ovfl(args[0], args[1]));
+        auto _seq3105_1 = m.mk_not(m_util.mk_bvsmul_no_udfl(args[0], args[1]));
+        result = m.mk_or(_seq3105_0, _seq3105_1);
+    }
     return BR_REWRITE_FULL;
 }
 
@@ -3271,7 +3345,11 @@ br_status bv_rewriter::mk_bvsdiv_overflow(unsigned num, expr * const * args, exp
     auto sz = get_bv_size(args[1]);
     auto minSigned = mk_numeral(rational::power_of_two(sz-1), sz);
     auto minusOne = mk_numeral(rational::power_of_two(sz) - 1, sz);
-    result = m.mk_and(m.mk_eq(args[0], minSigned), m.mk_eq(args[1], minusOne));
+    {
+        auto _seq3274_0 = m.mk_eq(args[0], minSigned);
+        auto _seq3274_1 = m.mk_eq(args[1], minusOne);
+        result = m.mk_and(_seq3274_0, _seq3274_1);
+    }
     return BR_REWRITE_FULL;
 }
 
diff --git a/src/ast/rewriter/enum2bv_rewriter.cpp b/src/ast/rewriter/enum2bv_rewriter.cpp
index 8210cdc931..699d320e82 100644
--- a/src/ast/rewriter/enum2bv_rewriter.cpp
+++ b/src/ast/rewriter/enum2bv_rewriter.cpp
@@ -73,9 +73,10 @@ struct enum2bv_rewriter::imp {
             unsigned domain_size = m_dt.get_datatype_num_constructors(s);
             if (is_unate(s)) {
                 expr_ref one(m_bv.mk_numeral(rational::one(), 1), m);
-                for (unsigned i = 0; i + 2 < domain_size; ++i) {                    
-                    bounds.push_back(m.mk_implies(m.mk_eq(one, m_bv.mk_extract(i + 1, i + 1, x)),
-                                                          m.mk_eq(one, m_bv.mk_extract(i, i, x))));
+                for (unsigned i = 0; i + 2 < domain_size; ++i) {
+                    auto _seq77_0 = m.mk_eq(one, m_bv.mk_extract(i + 1, i + 1, x));
+                    auto _seq77_1 = m.mk_eq(one, m_bv.mk_extract(i, i, x));
+                    bounds.push_back(m.mk_implies(_seq77_0, _seq77_1));
                 }
             }
             else {
@@ -167,7 +168,9 @@ struct enum2bv_rewriter::imp {
                 ptr_vector<func_decl> const& cs = *m_dt.get_datatype_constructors(s);
                 f_def = m.mk_const(cs[nc-1]);
                 for (unsigned i = nc - 1; i-- > 0; ) {
-                    f_def = m.mk_ite(m.mk_eq(result, value2bv(i, s)), m.mk_const(cs[i]), f_def);
+                    auto _seq170_0 = m.mk_eq(result, value2bv(i, s));
+                    auto _seq170_1 = m.mk_const(cs[i]);
+                    f_def = m.mk_ite(_seq170_0, _seq170_1, f_def);
                 }
                 m_imp.m_enum2def.insert(f, f_def);
                 m_imp.m_enum2bv.insert(f, f_fresh);
diff --git a/src/ast/rewriter/factor_rewriter.cpp b/src/ast/rewriter/factor_rewriter.cpp
index 89354b2369..0955f2598d 100644
--- a/src/ast/rewriter/factor_rewriter.cpp
+++ b/src/ast/rewriter/factor_rewriter.cpp
@@ -141,8 +141,16 @@ void factor_rewriter::mk_is_negative(expr_ref& result, expr_ref_vector& eqs) {
                 pos0 = pos;
             }
             else {
-                tmp = m().mk_or(m().mk_and(pos, pos0), m().mk_and(neg, neg0));
-                neg0 = m().mk_or(m().mk_and(neg, pos0), m().mk_and(pos, neg0));
+                {
+                    auto _seq144_0 = m().mk_and(pos, pos0);
+                    auto _seq144_1 = m().mk_and(neg, neg0);
+                    tmp = m().mk_or(_seq144_0, _seq144_1);
+                }
+                {
+                    auto _seq145_0 = m().mk_and(neg, pos0);
+                    auto _seq145_1 = m().mk_and(pos, neg0);
+                    neg0 = m().mk_or(_seq145_0, _seq145_1);
+                }
                 pos0 = tmp;
             }
         }
diff --git a/src/ast/rewriter/finite_set_axioms.cpp b/src/ast/rewriter/finite_set_axioms.cpp
index 5392ba7426..98824a22b1 100644
--- a/src/ast/rewriter/finite_set_axioms.cpp
+++ b/src/ast/rewriter/finite_set_axioms.cpp
@@ -219,8 +219,12 @@ void finite_set_axioms::in_range_axiom(expr *x, expr *a) {
     
     arith_util arith(m);
     expr_ref x_in_a(u.mk_in(x, a), m);
-    expr_ref lo_le_x(arith.mk_le(arith.mk_sub(lo, x), arith.mk_int(0)), m);
-    expr_ref x_le_hi(arith.mk_le(arith.mk_sub(x, hi), arith.mk_int(0)), m);
+    auto _seqa0 = arith.mk_sub(lo, x);
+    auto _seqa1 = arith.mk_int(0);
+    expr_ref lo_le_x(arith.mk_le(_seqa0, _seqa1), m);
+    auto _seqb0 = arith.mk_sub(x, hi);
+    auto _seqb1 = arith.mk_int(0);
+    expr_ref x_le_hi(arith.mk_le(_seqb0, _seqb1), m);
     m_rewriter(lo_le_x);
     m_rewriter(x_le_hi);
     expr_ref nx_le_hi(m.mk_not(x_le_hi), m);
@@ -247,7 +251,9 @@ void finite_set_axioms::in_range_axiom(expr* r) {
         return;
 
     arith_util a(m);
-    expr_ref lo_le_hi(a.mk_le(a.mk_sub(lo, hi), a.mk_int(0)), m);
+    auto _seq0 = a.mk_sub(lo, hi);
+    auto _seq1 = a.mk_int(0);
+    expr_ref lo_le_hi(a.mk_le(_seq0, _seq1), m);
     m_rewriter(lo_le_hi);
 
     add_binary("range-bounds", r, nullptr, m.mk_not(lo_le_hi), u.mk_in(lo, r));
@@ -339,7 +345,11 @@ void finite_set_axioms::size_ub_axiom(expr *sz) {
     else if (u.is_empty(e)) 
         add_unit("size", e, m.mk_eq(sz, a.mk_int(0)));    
     else if (u.is_union(e, x, y)) {
-        ineq = a.mk_le(sz, a.mk_add(u.mk_size(x), u.mk_size(y)));
+        {
+            auto _seq342_0 = u.mk_size(x);
+            auto _seq342_1 = u.mk_size(y);
+            ineq = a.mk_le(sz, a.mk_add(_seq342_0, _seq342_1));
+        }
         m_rewriter(ineq);
         add_unit("size", e, ineq);
     }
@@ -367,7 +377,14 @@ void finite_set_axioms::size_ub_axiom(expr *sz) {
         add_unit("size", e, ineq);
     }
     else if (u.is_range(e, x, y)) {
-        ineq = a.mk_eq(sz, m.mk_ite(a.mk_le(x, y), a.mk_add(a.mk_sub(y, x), a.mk_int(1)), a.mk_int(0)));
+        {
+            auto _seq370_0 = a.mk_le(x, y);
+            auto _seq376_0 = a.mk_sub(y, x);
+            auto _seq376_1 = a.mk_int(1);
+            auto _seq370_1 = a.mk_add(_seq376_0, _seq376_1);
+            auto _seq370_2 = a.mk_int(0);
+            ineq = a.mk_eq(sz, m.mk_ite(_seq370_0, _seq370_1, _seq370_2));
+        }
         m_rewriter(ineq);
         add_unit("size", e, ineq);
     }    
diff --git a/src/ast/rewriter/finite_set_rewriter.cpp b/src/ast/rewriter/finite_set_rewriter.cpp
index b86f211f1e..d84edab778 100644
--- a/src/ast/rewriter/finite_set_rewriter.cpp
+++ b/src/ast/rewriter/finite_set_rewriter.cpp
@@ -204,8 +204,16 @@ br_status finite_set_rewriter::mk_size(expr * arg, expr_ref & result) {
     if (u.is_range(arg, lower, upper)) {
         // size(range(a, b)) -> b - a + 1
         expr_ref size_expr(m);
-        size_expr = a.mk_add(a.mk_sub(upper, lower), a.mk_int(1));
-        result = m.mk_ite(a.mk_gt(lower, upper), a.mk_int(0), size_expr);
+        {
+            auto _seq207_0 = a.mk_sub(upper, lower);
+            auto _seq207_1 = a.mk_int(1);
+            size_expr = a.mk_add(_seq207_0, _seq207_1);
+        }
+        {
+            auto _seq208_0 = a.mk_gt(lower, upper);
+            auto _seq208_1 = a.mk_int(0);
+            result = m.mk_ite(_seq208_0, _seq208_1, size_expr);
+        }
         return BR_REWRITE3;
     }
     // Size is already in normal form, no simplifications
@@ -234,7 +242,11 @@ br_status finite_set_rewriter::mk_in(expr * elem, expr * set, expr_ref & result)
     expr *lo = nullptr, *hi = nullptr;
     if (u.is_range(set, lo, hi)) {
         arith_util a(m);
-        result = m.mk_and(a.mk_le(lo, elem), a.mk_le(elem, hi));
+        {
+            auto _seq237_0 = a.mk_le(lo, elem);
+            auto _seq237_1 = a.mk_le(elem, hi);
+            result = m.mk_and(_seq237_0, _seq237_1);
+        }
         return BR_REWRITE2;
     }
     // NB we don't rewrite (set.in x (set.union s t)) to (or (set.in x s) (set.in x t))
diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp
index 3be70d4057..f7308be21b 100644
--- a/src/ast/rewriter/fpa_rewriter.cpp
+++ b/src/ast/rewriter/fpa_rewriter.cpp
@@ -493,8 +493,11 @@ br_status fpa_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) {
         return BR_DONE;
     }
     if (m_util.is_ninf(arg1)) {
-        // -oo < arg2 -->  not(arg2 = -oo) and not(arg2 = NaN)
-        result = m().mk_and(m().mk_not(m().mk_eq(arg2, arg1)), mk_neq_nan(arg2));
+        {
+            auto _seq497_0 = m().mk_not(m().mk_eq(arg2, arg1));
+            auto _seq497_1 = mk_neq_nan(arg2);
+            result = m().mk_and(_seq497_0, _seq497_1);
+        }
         return BR_REWRITE3;
     }
     if (m_util.is_ninf(arg2)) {
@@ -508,8 +511,11 @@ br_status fpa_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) {
         return BR_DONE;
     }
     if (m_util.is_pinf(arg2)) {
-        // arg1 < +oo --> not(arg1 = +oo) and not(arg1 = NaN)
-        result = m().mk_and(m().mk_not(m().mk_eq(arg1, arg2)), mk_neq_nan(arg1));
+        {
+            auto _seq512_0 = m().mk_not(m().mk_eq(arg1, arg2));
+            auto _seq512_1 = mk_neq_nan(arg1);
+            result = m().mk_and(_seq512_0, _seq512_1);
+        }
         return BR_REWRITE3;
     }
 
diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp
index 95d06f3a22..6c566edaff 100644
--- a/src/ast/rewriter/pb2bv_rewriter.cpp
+++ b/src/ast/rewriter/pb2bv_rewriter.cpp
@@ -618,7 +618,11 @@ struct pb2bv_rewriter::imp {
                 return expr_ref(m.mk_true(), m);
             }
             expr_ref_vector fmls(m);
-            fmls.push_back(m.mk_implies(m.mk_not(out[0]), mk_seg_le_rec(outs, coeffs, i + 1, k)));
+            {
+                auto _seq621_0 = m.mk_not(out[0]);
+                auto _seq621_1 = mk_seg_le_rec(outs, coeffs, i + 1, k);
+                fmls.push_back(m.mk_implies(_seq621_0, _seq621_1));
+            }
             rational k1;
             for (unsigned j = 0; j + 1 < out.size(); ++j) {
                 k1 = k - rational(j+1)*c;
@@ -626,7 +630,11 @@ struct pb2bv_rewriter::imp {
                     fmls.push_back(m.mk_not(out[j]));
                     break;
                 }
-                fmls.push_back(m.mk_implies(m.mk_and(out[j], m.mk_not(out[j+1])), mk_seg_le_rec(outs, coeffs, i + 1, k1)));
+                {
+                    auto _seq629_0 = m.mk_and(out[j], m.mk_not(out[j + 1]));
+                    auto _seq629_1 = mk_seg_le_rec(outs, coeffs, i + 1, k1);
+                    fmls.push_back(m.mk_implies(_seq629_0, _seq629_1));
+                }
             }
             return ::mk_and(fmls);
         }
diff --git a/src/ast/rewriter/quant_hoist.cpp b/src/ast/rewriter/quant_hoist.cpp
index 7b1c25cf1c..ddbcd7e9b8 100644
--- a/src/ast/rewriter/quant_hoist.cpp
+++ b/src/ast/rewriter/quant_hoist.cpp
@@ -249,7 +249,11 @@ private:
                     pull_quantifier(t1, qt, vars, tt1, use_fresh, rewrite_ok);
                     nt1 = m.mk_not(t1);
                     pull_quantifier(nt1, qt, vars, ntt1, use_fresh, rewrite_ok);
-                    result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(tt1, tt3));
+                    {
+                        auto _seq252_0 = m.mk_or(ntt1, tt2);
+                        auto _seq252_1 = m.mk_or(tt1, tt3);
+                        result = m.mk_and(_seq252_0, _seq252_1);
+                    }
                 }
                 else {
                     result = m.mk_ite(t1, tt2, tt3);
@@ -263,7 +267,11 @@ private:
                 nt2 = m.mk_not(t2);
                 pull_quantifier(nt1, qt, vars, ntt1, use_fresh, rewrite_ok);
                 pull_quantifier(nt2, qt, vars, ntt2, use_fresh, rewrite_ok);
-                result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(ntt2, tt1));
+                {
+                    auto _seq266_0 = m.mk_or(ntt1, tt2);
+                    auto _seq266_1 = m.mk_or(ntt2, tt1);
+                    result = m.mk_and(_seq266_0, _seq266_1);
+                }
             }
             else {
                 // the formula contains a quantifier, but it is "inaccessible"
diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp
index 5d38ca2ddb..404884aac4 100644
--- a/src/ast/rewriter/seq_axioms.cpp
+++ b/src/ast/rewriter/seq_axioms.cpp
@@ -284,7 +284,11 @@ namespace seq {
             return false;
         }
         expr_ref l2(m), l1(l, m);
-        l2 = mk_sub(mk_len(s), a.mk_int(1));
+        {
+            auto _seq287_0 = mk_len(s);
+            auto _seq287_1 = a.mk_int(1);
+            l2 = mk_sub(_seq287_0, _seq287_1);
+        }
         m_rewrite(l1);
         m_rewrite(l2);
         return l1 == l2;
@@ -309,7 +313,11 @@ namespace seq {
         if (!a.is_numeral(i, i1) || !i1.is_one()) 
             return false;
         expr_ref l2(m), l1(l, m);
-        l2 = mk_sub(mk_len(s), a.mk_int(1));
+        {
+            auto _seq312_0 = mk_len(s);
+            auto _seq312_1 = a.mk_int(1);
+            l2 = mk_sub(_seq312_0, _seq312_1);
+        }
         m_rewrite(l1);
         m_rewrite(l2);
         return l1 == l2;
@@ -472,8 +480,11 @@ namespace seq {
             expr_ref len_s = mk_len(s);
             expr_ref mone(a.mk_int(-1), m);
             add_clause(~cnt, s_eq_empty, ~mk_literal(seq.str.mk_contains(seq.str.mk_substr(t,zero,a.mk_add(i,len_s,mone)),s)));
-            add_clause(~cnt, s_eq_empty, mk_seq_eq(seq.str.mk_substr(t,zero,a.mk_add(i,len_s)),
-                                                  seq.str.mk_concat(seq.str.mk_substr(t,zero,i), s)));
+            {
+                auto _seq475_0 = seq.str.mk_substr(t, zero, a.mk_add(i, len_s));
+                auto _seq475_1 = seq.str.mk_concat(seq.str.mk_substr(t, zero, i), s);
+                add_clause(~cnt, s_eq_empty, mk_seq_eq(_seq475_0, _seq475_1));
+            }
 #endif
         }
         else {
@@ -712,9 +723,13 @@ namespace seq {
         TRACE(seq, tout << mk_pp(e, m) << "\n";);
         expr_ref ge0 = mk_ge(e, 0);      
         expr* s = nullptr;
-        VERIFY (seq.str.is_stoi(e, s));    
-        add_clause(mk_ge(e, -1));                             // stoi(s) >= -1
-        add_clause(mk_eq(seq.str.mk_stoi(seq.str.mk_empty(s->get_sort())), a.mk_int(-1)));
+        VERIFY (seq.str.is_stoi(e, s));
+        add_clause(mk_ge(e, -1));
+        {
+            auto _seq717_0 = seq.str.mk_stoi(seq.str.mk_empty(s->get_sort()));
+            auto _seq717_1 = a.mk_int(-1);
+            add_clause(mk_eq(_seq717_0, _seq717_1));
+        }
 //      add_clause(~mk_eq_empty(s), mk_eq(e, a.mk_int(-1)));  // s = "" => stoi(s) = -1
         add_clause(~ge0, is_digit(mk_nth(s, 0)));             // stoi(s) >= 0 => is_digit(nth(s,0))
         add_clause(~ge0, mk_ge(mk_len(s), 1));                // stoi(s) >= 0 => len(s) >= 1
@@ -801,7 +816,11 @@ namespace seq {
             p *= 10;
         }
         es.reverse();
-        eq = m.mk_eq(seq.str.mk_ubv2s(b), seq.str.mk_concat(es, seq.str.mk_string_sort()));
+        {
+            auto _seq804_0 = seq.str.mk_ubv2s(b);
+            auto _seq804_1 = seq.str.mk_concat(es, seq.str.mk_string_sort());
+            eq = m.mk_eq(_seq804_0, _seq804_1);
+        }
         SASSERT(pow < rational::power_of_two(sz));
         if (k == 0)
             add_clause(ge10k1, eq);
@@ -873,7 +892,11 @@ namespace seq {
         expr_ref eq(m);
         unsigned sz = bv.get_bv_size(bv_sort);
         for (unsigned i = 0; i < 10; ++i) {
-            eq = m.mk_eq(m_sk.mk_ubv2ch(bv.mk_numeral(i, sz)), seq.mk_char('0' + i));
+            {
+                auto _seq876_0 = m_sk.mk_ubv2ch(bv.mk_numeral(i, sz));
+                auto _seq876_1 = seq.mk_char('0' + i);
+                eq = m.mk_eq(_seq876_0, _seq876_1);
+            }
             add_clause(eq);
         }
     }
@@ -1015,8 +1038,10 @@ namespace seq {
     */
     void axioms::str_to_code_axiom(expr* n) {
         expr* e = nullptr;
-        VERIFY(seq.str.is_to_code(n, e)); 
-        expr_ref len_is1 = mk_eq(mk_len(e), a.mk_int(1));
+        VERIFY(seq.str.is_to_code(n, e));
+        auto _seq1019_0 = mk_len(e);
+        auto _seq1019_1 = a.mk_int(1);
+        expr_ref len_is1 = mk_eq(_seq1019_0, _seq1019_1);
         add_clause(~len_is1, mk_ge(n, 0)); 
         add_clause(~len_is1, mk_le(n, seq.max_char()));
         add_clause(~len_is1, mk_eq(n, seq.mk_char2int(mk_nth(e, 0))));
@@ -1036,7 +1061,11 @@ namespace seq {
         expr_ref ge = mk_ge(e, 0);
         expr_ref le = mk_le(e, seq.max_char());
         expr_ref emp = expr_ref(seq.str.mk_is_empty(n), m);
-        add_clause(~ge, ~le, mk_eq(mk_len(n), a.mk_int(1)));
+        {
+            auto _seq1039_0 = mk_len(n);
+            auto _seq1039_1 = a.mk_int(1);
+            add_clause(~ge, ~le, mk_eq(_seq1039_0, _seq1039_1));
+        }
         if (!seq.str.is_to_code(e))
             add_clause(~ge, ~le, mk_eq(seq.str.mk_to_code(n), e));
         add_clause(ge, emp);
@@ -1105,7 +1134,10 @@ namespace seq {
         expr_ref len_r(seq.str.mk_length(vr), m);
         expr_ref test1(m.mk_eq(len_s, vi), m);
         expr_ref branch1(m.mk_eq(len_r, vj), m);
-        expr_ref test2(m.mk_and(a.mk_gt(len_s, vi), m.mk_eq(vi, a.mk_int(0)), seq.str.mk_is_empty(vp)), m);
+        auto _seqt0 = a.mk_gt(len_s, vi);
+        auto _seqt1 = m.mk_eq(vi, a.mk_int(0));
+        auto _seqt2 = seq.str.mk_is_empty(vp);
+        expr_ref test2(m.mk_and(_seqt0, _seqt1, _seqt2), m);
         expr_ref branch2(m.mk_eq(vr, seq.str.mk_concat(vt, vs)), m);
         throw default_exception("no support for replace-all");
 #if 0
@@ -1176,12 +1208,20 @@ namespace seq {
         auto s = purify(_s);
         auto t = purify(_t);
         expr_ref lit = expr_ref(e, m);
-        expr_ref s_gt_t = mk_ge(mk_sub(mk_len(s), mk_len(t)), 1);
+        auto _seql0 = mk_len(s);
+        auto _seql1 = mk_len(t);
+        expr_ref s_gt_t = mk_ge(mk_sub(_seql0, _seql1), 1);
 #if 0
         expr_ref x = m_sk.mk_pre(t, mk_sub(mk_len(t), mk_len(s)));
-        expr_ref y = m_sk.mk_tail(t, mk_sub(mk_len(s), a.mk_int(1)));
+        auto _seq1182_0 = mk_len(s);
+        auto _seq1182_1 = a.mk_int(1);
+        expr_ref y = m_sk.mk_tail(t, mk_sub(_seq1182_0, _seq1182_1));
         add_clause(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, y)));
-        add_clause(lit, s_gt_t, mk_eq(mk_len(y), mk_len(s)));
+        {
+            auto _seq1184_0 = mk_len(y);
+            auto _seq1184_1 = mk_len(s);
+            add_clause(lit, s_gt_t, mk_eq(_seq1184_0, _seq1184_1));
+        }
         add_clause(lit, s_gt_t, ~mk_eq(y, s));    
 #else
         sort* char_sort = nullptr;
@@ -1203,12 +1243,21 @@ namespace seq {
         auto s = purify(_s);
         auto t = purify(_t);
         expr_ref lit = expr_ref(e, m);
-        expr_ref s_gt_t = mk_ge(mk_sub(mk_len(s), mk_len(t)), 1);
+        auto _seql0 = mk_len(s);
+        auto _seql1 = mk_len(t);
+        expr_ref s_gt_t = mk_ge(mk_sub(_seql0, _seql1), 1);
 #if 0
-        expr_ref x = m_sk.mk_pre(t, mk_len(s));    
-        expr_ref y = m_sk.mk_tail(t, mk_sub(mk_sub(mk_len(t), mk_len(s)), a.mk_int(1)));
+        expr_ref x = m_sk.mk_pre(t, mk_len(s));    auto _seq1241_0 = mk_len(t);
+    auto _seq1241_1 = mk_len(s);
+    auto _seq1209_0 = mk_sub(_seq1241_0, _seq1241_1);
+    auto _seq1209_1 = a.mk_int(1);
+    expr_ref y = m_sk.mk_tail(t, mk_sub(_seq1209_0, _seq1209_1));
         add_clause(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, y)));
-        add_clause(lit, s_gt_t, mk_eq(mk_len(x), mk_len(s)));
+        {
+            auto _seq1211_0 = mk_len(x);
+            auto _seq1211_1 = mk_len(s);
+            add_clause(lit, s_gt_t, mk_eq(_seq1211_0, _seq1211_1));
+        }
         add_clause(lit, s_gt_t, ~mk_eq(x, s));
 
 #else
diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp
index bd39e042a3..f0cd0aee9f 100644
--- a/src/ast/rewriter/seq_derive.cpp
+++ b/src/ast/rewriter/seq_derive.cpp
@@ -412,8 +412,11 @@ namespace seq {
                 in_range = m_util.mk_le(m_ele, c_hi);
             else if (hi_trivial)
                 in_range = m_util.mk_le(c_lo, m_ele);
-            else
-                in_range = m.mk_and(m_util.mk_le(c_lo, m_ele), m_util.mk_le(m_ele, c_hi));
+            else {
+                auto _seq416_0 = m_util.mk_le(c_lo, m_ele);
+                auto _seq416_1 = m_util.mk_le(m_ele, c_hi);
+                in_range = m.mk_and(_seq416_0, _seq416_1);
+            }
 
             return mk_ite(in_range, eps, empty);
         }
@@ -477,26 +480,27 @@ namespace seq {
             result = re().mk_reverse(r);
         else if (re().is_reverse(r, r1))
             result = r1;
-        else if (re().is_concat(r, r1, r2))
-            result = re().mk_concat(mk_regex_reverse(r2), mk_regex_reverse(r1));
-        else if (m.is_ite(r, c, r1, r2))
-            result = m.mk_ite(c, mk_regex_reverse(r1), mk_regex_reverse(r2));
-        else if (re().is_union(r, r1, r2)) {
+        else if (re().is_concat(r, r1, r2)) {
+            auto _seq0 = mk_regex_reverse(r2);
+            auto _seq1 = mk_regex_reverse(r1);
+            result = re().mk_concat(_seq0, _seq1);
+        } else if (m.is_ite(r, c, r1, r2)) {
+            auto _seq0 = mk_regex_reverse(r1);
+            auto _seq1 = mk_regex_reverse(r2);
+            result = m.mk_ite(c, _seq0, _seq1);
+        } else if (re().is_union(r, r1, r2)) {
             auto a1 = mk_regex_reverse(r1);
             auto b1 = mk_regex_reverse(r2);
             result = re().mk_union(a1, b1);
-        }
-        else if (re().is_intersection(r, r1, r2)) {
+        } else if (re().is_intersection(r, r1, r2)) {
             auto a1 = mk_regex_reverse(r1);
             auto b1 = mk_regex_reverse(r2);
             result = re().mk_inter(a1, b1);
-        }
-        else if (re().is_diff(r, r1, r2)) {
+        } else if (re().is_diff(r, r1, r2)) {
             auto a1 = mk_regex_reverse(r1);
             auto b1 = mk_regex_reverse(r2);
             result = re().mk_diff(a1, b1);
-        }
-        else if (re().is_star(r, r1))
+        } else if (re().is_star(r, r1))
             result = re().mk_star(mk_regex_reverse(r1));
         else if (re().is_plus(r, r1))
             result = re().mk_plus(mk_regex_reverse(r1));
@@ -821,7 +825,11 @@ namespace seq {
                 if (m.is_ite(e, c1, t1, el1) && m.is_ite(s, c2, t2, el2) && c1 == c2) {
                     set.set(i, set.back());
                     set.pop_back();
-                    e = mk_ite(c1, mk_union(t1, t2), mk_union(el1, el2));
+                    {
+                        auto _seq824_0 = mk_union(t1, t2);
+                        auto _seq824_1 = mk_union(el1, el2);
+                        e = mk_ite(c1, _seq824_0, _seq824_1);
+                    }
                     changed = true;
                     break;
                 }
@@ -880,10 +888,16 @@ namespace seq {
         // nested inter/union leaves, so states stay ground either way.
         expr *u1 = nullptr, *u2 = nullptr;
         if (m_derivative_kind == derivative_kind::antimirov_t) {
-            if (re().is_union(a, u1, u2))
-                return mk_union(mk_inter(u1, b), mk_inter(u2, b));
-            if (re().is_union(b, u1, u2))
-                return mk_union(mk_inter(a, u1), mk_inter(a, u2));
+            if (re().is_union(a, u1, u2)) {
+                auto _seq0 = mk_inter(u1, b);
+                auto _seq1 = mk_inter(u2, b);
+                return mk_union(_seq0, _seq1);
+            }
+            if (re().is_union(b, u1, u2)) {
+                auto _seq0 = mk_inter(a, u1);
+                auto _seq1 = mk_inter(a, u2);
+                return mk_union(_seq0, _seq1);
+            }
         }
 
         // Base case: build raw intersection
@@ -981,10 +995,16 @@ namespace seq {
         // state is shared rather than growing into ~(Σ*a ∪ ε ∪ ...), which
         // otherwise defeats dead-state detection on loop ∩ comp regexes.
         expr* e1 = nullptr, *e2 = nullptr;
-        if (re().is_union(a, e1, e2))
-            return mk_inter(mk_complement(e1), mk_complement(e2));
-        if (re().is_intersection(a, e1, e2))
-            return mk_union(mk_complement(e1), mk_complement(e2));
+        if (re().is_union(a, e1, e2)) {
+            auto _seq0 = mk_complement(e1);
+            auto _seq1 = mk_complement(e2);
+            return mk_inter(_seq0, _seq1);
+        }
+        if (re().is_intersection(a, e1, e2)) {
+            auto _seq0 = mk_complement(e1);
+            auto _seq1 = mk_complement(e2);
+            return mk_union(_seq0, _seq1);
+        }
 
         return expr_ref(re().mk_complement(a), m);
     }
diff --git a/src/ast/rewriter/seq_eq_solver.cpp b/src/ast/rewriter/seq_eq_solver.cpp
index a77aaa55ba..73b814fd60 100644
--- a/src/ast/rewriter/seq_eq_solver.cpp
+++ b/src/ast/rewriter/seq_eq_solver.cpp
@@ -408,7 +408,9 @@ namespace seq {
             return true;
         }
 
-        expr_ref eq_length(m.mk_eq(a.mk_int(lenX), seq.str.mk_length(X)), m);
+        auto _seq0 = a.mk_int(lenX);
+        auto _seq1 = seq.str.mk_length(X);
+        expr_ref eq_length(m.mk_eq(_seq0, _seq1), m);
         expr* val = ctx.expr2rep(eq_length);
         if (!m.is_false(val)) {
             expr_ref Y(seq.str.mk_concat(lenX.get_unsigned(), units.data(), X->get_sort()), m);
diff --git a/src/ast/rewriter/seq_range_collapse.cpp b/src/ast/rewriter/seq_range_collapse.cpp
index 6e64274810..8206ef5c1f 100644
--- a/src/ast/rewriter/seq_range_collapse.cpp
+++ b/src/ast/rewriter/seq_range_collapse.cpp
@@ -248,7 +248,11 @@ namespace seq {
         auto &ch = u.get_char_plugin();
         for (unsigned i = 0; i < n; ++i) {
             auto [lo, hi] = p[i];
-            ranges.push_back(m.mk_and(ch.mk_le(ch.mk_char(lo), bound), ch.mk_le(bound, ch.mk_char(hi))));
+            {
+                auto _seq251_0 = ch.mk_le(ch.mk_char(lo), bound);
+                auto _seq251_1 = ch.mk_le(bound, ch.mk_char(hi));
+                ranges.push_back(m.mk_and(_seq251_0, _seq251_1));
+            }
         }
         expr_ref body(m.mk_or(ranges), m);
         auto lam = m.mk_lambda(1, &char_sort, &char_sym, body);
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 79c542f06b..af45569b40 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -936,7 +936,11 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
     expr* a1 = nullptr, *b1 = nullptr, *c1 = nullptr;
     if (str().is_extract(a, a1, b1, c1) && 
         is_suffix(a1, b1, c1) && is_suffix(a, b, c)) {
-        result = str().mk_substr(a1, m_autil.mk_add(b1, b), m_autil.mk_sub(c1, b));
+        {
+            auto _seq939_0 = m_autil.mk_add(b1, b);
+            auto _seq939_1 = m_autil.mk_sub(c1, b);
+            result = str().mk_substr(a1, _seq939_0, _seq939_1);
+        }
         return BR_REWRITE3;
     }
     rational r1, r2;
@@ -957,7 +961,11 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
         if (r1 >= 0 && pos <= r2) {
             r2 = std::min(r2 - pos, len);
             r1 += pos;
-            result = str().mk_substr(a1, m_autil.mk_numeral(r1, true), m_autil.mk_numeral(r2, true));
+            {
+                auto _seq960_0 = m_autil.mk_numeral(r1, true);
+                auto _seq960_1 = m_autil.mk_numeral(r2, true);
+                result = str().mk_substr(a1, _seq960_0, _seq960_1);
+            }
             return BR_REWRITE1;
         }
     }
@@ -990,7 +998,11 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
     // extract(extract(a, 3, 6), 1, len(extract(a, 3, 6)) - 1) -> extract(a, 4, 5)
     if (str().is_extract(a, a1, b1, c1) && is_suffix(a, b, c) && 
         m_autil.is_numeral(c1) && m_autil.is_numeral(b1)) {
-        result = str().mk_substr(a1, m_autil.mk_add(b, b1), m_autil.mk_sub(c1, b));
+        {
+            auto _seq993_0 = m_autil.mk_add(b, b1);
+            auto _seq993_1 = m_autil.mk_sub(c1, b);
+            result = str().mk_substr(a1, _seq993_0, _seq993_1);
+        }
         return BR_REWRITE2;
     }
  
@@ -1008,9 +1020,9 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
     if (pos == 0 && as.forall(is_unit)) {
         result = str().mk_empty(a->get_sort());
         for (unsigned i = 1; i <= as.size(); ++i) {
-            result = m().mk_ite(m_autil.mk_ge(c, m_autil.mk_int(i)), 
-                                str().mk_concat(i, as.data(), a->get_sort()), 
-                                result);
+            auto _seq1011_0 = m_autil.mk_ge(c, m_autil.mk_int(i));
+            auto _seq1011_1 = str().mk_concat(i, as.data(), a->get_sort());
+            result = m().mk_ite(_seq1011_0, _seq1011_1, result);
         }
         return BR_REWRITE_FULL;
     }
@@ -1350,7 +1362,9 @@ br_status seq_rewriter::mk_seq_nth(expr* a, expr* b, expr_ref& result) {
             expr_ref case2(str().mk_nth_u(str().mk_empty(s->get_sort()), b), m());
             expr_ref case3(str().mk_nth_u(a, b), m());
             result = case3;
-            result = m().mk_ite(m_autil.mk_lt(m_autil.mk_add(k, b), str().mk_length(s)), case1, result);
+            auto _seq0 = m_autil.mk_add(k, b);
+            auto _seq1 = str().mk_length(s);
+            result = m().mk_ite(m_autil.mk_lt(_seq0, _seq1), case1, result);
             result = m().mk_ite(m_autil.mk_ge(k, str().mk_length(s)), case2, result);
             result = m().mk_ite(m_autil.mk_lt(b, zero()), case3, result);   
             return BR_REWRITE_FULL;
@@ -1489,9 +1503,12 @@ br_status seq_rewriter::mk_seq_last_index(expr* a, expr* b, expr_ref& result) {
             switch (is_suffix(as, bs)) {
             case l_undef:
                 return BR_FAILED;
-            case l_true:
-                result = m_autil.mk_sub(str().mk_length(a), m_autil.mk_int(bs.size() - i));
+            case l_true: {
+                auto _seq0 = str().mk_length(a);
+                auto _seq1 = m_autil.mk_int(bs.size() - i);
+                result = m_autil.mk_sub(_seq0, _seq1);
                 return BR_REWRITE3;
+            }
             case l_false:
                 as.pop_back();
                 --i;
@@ -1596,7 +1613,11 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result
             expr_ref a1(m());
             a1 = str().mk_concat(as.size() - i, as.data() + i, sort_a);
             result = str().mk_index(a1, b, m_autil.mk_int(r));
-            result = m().mk_ite(m_autil.mk_ge(result, zero()), m_autil.mk_add(m_autil.mk_int(i), result), minus_one());
+            {
+                auto _seq1599_0 = m_autil.mk_ge(result, zero());
+                auto _seq1599_1 = m_autil.mk_add(m_autil.mk_int(i), result);
+                result = m().mk_ite(_seq1599_0, _seq1599_1, minus_one());
+            }
             return BR_REWRITE_FULL;
         }
     }
@@ -1613,7 +1634,11 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result
     if (i > 0) {
         result = str().mk_index(
             str().mk_concat(as.size() - i, as.data() + i, sort_a), b, c);
-        result = m().mk_ite(m_autil.mk_ge(result, zero()), m_autil.mk_add(m_autil.mk_int(i), result), minus_one());
+        {
+            auto _seq1616_0 = m_autil.mk_ge(result, zero());
+            auto _seq1616_1 = m_autil.mk_add(m_autil.mk_int(i), result);
+            result = m().mk_ite(_seq1616_0, _seq1616_1, minus_one());
+        }
         return BR_REWRITE_FULL;
     }
 
@@ -1624,11 +1649,12 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result
             return BR_DONE;
         }
         break;
-    case same_length_c:
-        result = m().mk_ite(m_autil.mk_le(c, minus_one()), minus_one(), 
-                            m().mk_ite(m().mk_eq(c, zero()), 
-                                       m().mk_ite(m().mk_eq(a, b), zero(), minus_one()),
-                                       minus_one()));
+    case same_length_c: {
+        auto _seqa = m_autil.mk_le(c, minus_one());
+        auto _seqb = m().mk_eq(c, zero());
+        auto _seqc = m().mk_ite(m().mk_eq(a, b), zero(), minus_one());
+        result = m().mk_ite(_seqa, minus_one(), m().mk_ite(_seqb, _seqc, minus_one()));
+    }
         return BR_REWRITE_FULL;
     default:
         break;
@@ -1636,8 +1662,13 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result
     if (is_zero && !as.empty() && str().is_unit(as.get(0))) {
         expr_ref a1(str().mk_concat(as.size() - 1, as.data() + 1, as[0]->get_sort()), m());
         expr_ref b1(str().mk_index(a1, b, c), m());
-        result = m().mk_ite(str().mk_prefix(b, a), zero(), 
-                            m().mk_ite(m_autil.mk_ge(b1, zero()), m_autil.mk_add(one(), b1), minus_one()));
+        {
+            auto _seq1639_0 = str().mk_prefix(b, a);
+            auto _seq1663_0 = m_autil.mk_ge(b1, zero());
+            auto _seq1663_1 = m_autil.mk_add(one(), b1);
+            auto _seq1639_1 = m().mk_ite(_seq1663_0, _seq1663_1, minus_one());
+            result = m().mk_ite(_seq1639_0, zero(), _seq1639_1);
+        }
         return BR_REWRITE3;
     }
     expr_ref ra(a, m());
@@ -1780,7 +1811,11 @@ br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& resu
         if (cmp == l_true && m_lhs.size() < i + m_rhs.size()) {
             expr_ref a1(str().mk_concat(i, m_lhs.data(), sort_a), m());
             expr_ref a2(str().mk_concat(m_lhs.size()-i, m_lhs.data()+i, sort_a), m());
-            result = m().mk_ite(m().mk_eq(a2, b), str().mk_concat(a1, c), a);
+            {
+                auto _seq1783_0 = m().mk_eq(a2, b);
+                auto _seq1783_1 = str().mk_concat(a1, c);
+                result = m().mk_ite(_seq1783_0, _seq1783_1, a);
+            }
             return BR_REWRITE_FULL;            
         }
         if (cmp == l_true) {
@@ -1811,7 +1846,11 @@ br_status seq_rewriter::mk_seq_replace_all(expr* a, expr* b, expr* c, expr_ref&
         return BR_DONE;
     } 
     if (a == b) {
-        result = m().mk_ite(str().mk_is_empty(b), str().mk_empty(a->get_sort()), c);
+        {
+            auto _seq1814_0 = str().mk_is_empty(b);
+            auto _seq1814_1 = str().mk_empty(a->get_sort());
+            result = m().mk_ite(_seq1814_0, _seq1814_1, c);
+        }
         return BR_REWRITE2;
     }
     if (str().is_empty(a) && str().is_empty(c)) {
@@ -1908,10 +1947,16 @@ expr_ref seq_rewriter::re_replace_char(expr *r, unsigned a_ch, unsigned b_ch, ex
                     if (ch == a_ch || ch == b_ch) {
                         if (prev < ch) {
                             zstring prev_z(prev), pred_z(ch - 1);
-                            parts.push_back(re().mk_range(str().mk_string(prev_z), str().mk_string(pred_z)));
+                            {
+                                auto _seq1911_0 = str().mk_string(prev_z);
+                                auto _seq1911_1 = str().mk_string(pred_z);
+                                parts.push_back(re().mk_range(_seq1911_0, _seq1911_1));
+                            }
                         }
                         if (ch == b_ch) {
-                            parts.push_back(re().mk_union(re().mk_to_re(a_str), re().mk_to_re(b_str)));
+                            auto _seq1914_0 = re().mk_to_re(a_str);
+                            auto _seq1914_1 = re().mk_to_re(b_str);
+                            parts.push_back(re().mk_union(_seq1914_0, _seq1914_1));
                         }
                         // a_ch is simply excluded (not added)
                         prev = ch + 1;
@@ -1919,7 +1964,11 @@ expr_ref seq_rewriter::re_replace_char(expr *r, unsigned a_ch, unsigned b_ch, ex
                 }
                 if (prev <= hi) {
                     zstring prev_z(prev), hi_z(hi);
-                    parts.push_back(re().mk_range(str().mk_string(prev_z), str().mk_string(hi_z)));
+                    {
+                        auto _seq1922_0 = str().mk_string(prev_z);
+                        auto _seq1922_1 = str().mk_string(hi_z);
+                        parts.push_back(re().mk_range(_seq1922_0, _seq1922_1));
+                    }
                 }
             }
             if (parts.empty()) {
@@ -2153,8 +2202,11 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
                 SASSERT(as.size() > 1);
                 s2 = s2.extract(s1.length(), s2.length()-s1.length());
                 bs[0] = str().mk_string(s2);
-                result = str().mk_prefix(str().mk_concat(as.size()-1, as.data()+1, sort_a),
-                                              str().mk_concat(bs.size(), bs.data(), sort_a));
+                {
+                    auto _seq2156_0 = str().mk_concat(as.size() - 1, as.data() + 1, sort_a);
+                    auto _seq2156_1 = str().mk_concat(bs.size(), bs.data(), sort_a);
+                    result = str().mk_prefix(_seq2156_0, _seq2156_1);
+                }
                 TRACE(seq, tout << s1 << " " << s2 << " " << result << "\n";);
                 return BR_REWRITE_FULL;
             }
@@ -2446,13 +2498,14 @@ br_status seq_rewriter::mk_str_sbv2s(expr *a, expr_ref &result) {
     }
     
     bv_size = bv.get_bv_size(a);
-    result = m().mk_ite(
-        bv.mk_slt(a,bv.mk_numeral(0, bv_size)),
-        str().mk_concat(
-            str().mk_string(zstring("-")),
-            str().mk_ubv2s(bv.mk_bv_neg(a))
-        ),
-        str().mk_ubv2s(a));
+    {
+        auto _seq2449_0 = bv.mk_slt(a, bv.mk_numeral(0, bv_size));
+        auto _seq2499_0 = str().mk_string(zstring("-"));
+        auto _seq2499_1 = str().mk_ubv2s(bv.mk_bv_neg(a));
+        auto _seq2449_1 = str().mk_concat(_seq2499_0, _seq2499_1);
+        auto _seq2449_2 = str().mk_ubv2s(a);
+        result = m().mk_ite(_seq2449_0, _seq2449_1, _seq2449_2);
+    }
     return BR_REWRITE_FULL;
 }
 
@@ -2556,10 +2609,12 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
         expr_ref tail(str().mk_stoi(as.back()), m());
         expr_ref head(str().mk_concat(as.size() - 1, as.data(), a->get_sort()), m());
         expr_ref stoi_head(str().mk_stoi(head), m());
-        result = m().mk_ite(m_autil.mk_ge(stoi_head, zero()), 
-                            m_autil.mk_add(m_autil.mk_mul(m_autil.mk_int(10), stoi_head), tail),
-                            minus_one());
-        
+        {
+            auto _seq2559_0 = m_autil.mk_ge(stoi_head, zero());
+            auto _seq2559_1 = m_autil.mk_add(m_autil.mk_mul(m_autil.mk_int(10), stoi_head), tail);
+            result = m().mk_ite(_seq2559_0, _seq2559_1, minus_one());
+        }
+
         result = m().mk_ite(m_autil.mk_ge(tail, zero()), 
                             result,
                             tail);
@@ -2570,9 +2625,11 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
     }
     if (str().is_unit(as.get(0), u) && m_util.is_const_char(u, ch) && '0' == ch) {
         result = str().mk_concat(as.size() - 1, as.data() + 1, as[0]->get_sort());
-        result = m().mk_ite(str().mk_is_empty(result),
-                            zero(),
-                            str().mk_stoi(result));
+        {
+            auto _seq2573_0 = str().mk_is_empty(result);
+            auto _seq2573_1 = str().mk_stoi(result);
+            result = m().mk_ite(_seq2573_0, zero(), _seq2573_1);
+        }
         return BR_REWRITE_FULL;
     }
 
@@ -2781,7 +2838,11 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) {
         return BR_REWRITE2;
     }
     else if (m().is_ite(r, p, r1, r2)) {
-        result = m().mk_ite(p, re().mk_reverse(r1), re().mk_reverse(r2));
+        {
+            auto _seq2784_0 = re().mk_reverse(r1);
+            auto _seq2784_1 = re().mk_reverse(r2);
+            result = m().mk_ite(p, _seq2784_0, _seq2784_1);
+        }
         return BR_REWRITE2;
     }
     else if (re().is_opt(r, r1)) {
@@ -3214,8 +3275,11 @@ bool seq_rewriter::rewrite_contains_pattern(expr* a, expr* b, expr_ref& result)
                 suffix = re().mk_concat(suffix, re().mk_to_re(e));
             suffix = re().mk_concat(suffix, full);
         }
-        fmls.push_back(m().mk_and(re().mk_in_re(x, prefix),
-                                  re().mk_in_re(y, suffix)));
+        {
+            auto _seq3217_0 = re().mk_in_re(x, prefix);
+            auto _seq3217_1 = re().mk_in_re(y, suffix);
+            fmls.push_back(m().mk_and(_seq3217_0, _seq3217_1));
+        }
     }
     result = mk_or(fmls);
     return true;    
@@ -3420,7 +3484,9 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
 #if 0
     unsigned len = 0;
     if (has_fixed_length_constraint(b, len)) {
-        expr_ref len_lim(m().mk_eq(m_autil.mk_int(len), str().mk_length(a)), m());
+        auto _seq0 = m_autil.mk_int(len);
+        auto _seq1 = str().mk_length(a);
+        expr_ref len_lim(m().mk_eq(_seq0, _seq1), m());
         // this forces derivatives. Perhaps not a good thing for intersections.
         // alternative is to hoist out the smallest length constraining regex
         // and keep the result for the sequence expression that is kept without rewriting
@@ -3551,7 +3617,11 @@ br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) {
     expr* u1 = nullptr, *u2 = nullptr;
     if (re().is_full_seq(a) && re().is_union(b, u1, u2) &&
         (starts_with_full_seq(u1) || starts_with_full_seq(u2))) {
-        result = mk_regex_union_normalize(mk_regex_concat(a, u1), mk_regex_concat(a, u2));
+        {
+            auto _seq3554_0 = mk_regex_concat(a, u1);
+            auto _seq3554_1 = mk_regex_concat(a, u2);
+            result = mk_regex_union_normalize(_seq3554_0, _seq3554_1);
+        }
         return BR_REWRITE2;
     }
     if (re().is_intersection(a, u1, u2) && re().is_full_seq(b) &&
@@ -3645,11 +3715,19 @@ br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) {
     // Hoist ite out of concat: concat(ite(c, r1, r2), b) → ite(c, concat(r1, b), concat(r2, b))
     expr* c = nullptr;
     if (m().is_ite(a, c, a1, b1)) {
-        result = m().mk_ite(c, re().mk_concat(a1, b), re().mk_concat(b1, b));
+        {
+            auto _seq3648_0 = re().mk_concat(a1, b);
+            auto _seq3648_1 = re().mk_concat(b1, b);
+            result = m().mk_ite(c, _seq3648_0, _seq3648_1);
+        }
         return BR_REWRITE3;
     }
     if (m().is_ite(b, c, a1, b1)) {
-        result = m().mk_ite(c, re().mk_concat(a, a1), re().mk_concat(a, b1));
+        {
+            auto _seq3652_0 = re().mk_concat(a, a1);
+            auto _seq3652_1 = re().mk_concat(a, b1);
+            result = m().mk_ite(c, _seq3652_0, _seq3652_1);
+        }
         return BR_REWRITE3;
     }
     if (re().is_concat(a, a1, a2)) {
@@ -3783,11 +3861,19 @@ br_status seq_rewriter::mk_re_union0(expr* a, expr* b, expr_ref& result) {
     // Hoist ite out of union: union(ite(c, r1, r2), b) → ite(c, union(r1, b), union(r2, b))
     expr *c = nullptr, *r1 = nullptr, *r2 = nullptr;
     if (m().is_ite(a, c, r1, r2)) {
-        result = m().mk_ite(c, re().mk_union(r1, b), re().mk_union(r2, b));
+        {
+            auto _seq3786_0 = re().mk_union(r1, b);
+            auto _seq3786_1 = re().mk_union(r2, b);
+            result = m().mk_ite(c, _seq3786_0, _seq3786_1);
+        }
         return BR_REWRITE3;
     }
     if (m().is_ite(b, c, r1, r2)) {
-        result = m().mk_ite(c, re().mk_union(a, r1), re().mk_union(a, r2));
+        {
+            auto _seq3790_0 = re().mk_union(a, r1);
+            auto _seq3790_1 = re().mk_union(a, r2);
+            result = m().mk_ite(c, _seq3790_0, _seq3790_1);
+        }
         return BR_REWRITE3;
     }
     if (try_collapse_re_union(a, b, result))
@@ -3839,7 +3925,11 @@ br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
     // Hoist ite out of complement: ~(ite(c, r1, r2)) → ite(c, ~r1, ~r2)
     expr* c = nullptr;
     if (m().is_ite(a, c, e1, e2)) {
-        result = m().mk_ite(c, re().mk_complement(e1), re().mk_complement(e2));
+        {
+            auto _seq3842_0 = re().mk_complement(e1);
+            auto _seq3842_1 = re().mk_complement(e2);
+            result = m().mk_ite(c, _seq3842_0, _seq3842_1);
+        }
         return BR_REWRITE3;
     }
     return BR_FAILED;
@@ -3875,11 +3965,19 @@ br_status seq_rewriter::mk_re_inter0(expr* a, expr* b, expr_ref& result) {
     // Hoist ite out of intersection: inter(ite(c, r1, r2), b) → ite(c, inter(r1, b), inter(r2, b))
     expr *c = nullptr, *r1 = nullptr, *r2 = nullptr;
     if (m().is_ite(a, c, r1, r2)) {
-        result = m().mk_ite(c, re().mk_inter(r1, b), re().mk_inter(r2, b));
+        {
+            auto _seq3878_0 = re().mk_inter(r1, b);
+            auto _seq3878_1 = re().mk_inter(r2, b);
+            result = m().mk_ite(c, _seq3878_0, _seq3878_1);
+        }
         return BR_REWRITE3;
     }
     if (m().is_ite(b, c, r1, r2)) {
-        result = m().mk_ite(c, re().mk_inter(a, r1), re().mk_inter(a, r2));
+        {
+            auto _seq3882_0 = re().mk_inter(a, r1);
+            auto _seq3882_1 = re().mk_inter(a, r2);
+            result = m().mk_ite(c, _seq3882_0, _seq3882_1);
+        }
         return BR_REWRITE3;
     }
     if (try_collapse_re_inter(a, b, result))
@@ -4133,8 +4231,11 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
             result = re().mk_full_seq(b1->get_sort());
             return BR_REWRITE2;
         }
-        // Hoist ite out of star: (ite c r1 r2)* → ite(c, r1*, r2*)
-        result = m().mk_ite(c, re().mk_star(b1), re().mk_star(c1));
+        {
+            auto _seq4137_0 = re().mk_star(b1);
+            auto _seq4137_1 = re().mk_star(c1);
+            result = m().mk_ite(c, _seq4137_0, _seq4137_1);
+        }
         return BR_REWRITE3;
     }
     return BR_FAILED;
@@ -4837,8 +4938,11 @@ bool seq_rewriter::reduce_contains(expr* a, expr* b, expr_ref_vector& disj) {
 
         if (str().is_string(b, s)) {
             expr* all = re().mk_full_seq(re().mk_re(b->get_sort()));
-            disj.push_back(re().mk_in_re(str().mk_concat(m_lhs.size() - i, m_lhs.data() + i, sort_a),
-                                              re().mk_concat(all, re().mk_concat(re().mk_to_re(b), all))));
+            {
+                auto _seq4840_0 = str().mk_concat(m_lhs.size() - i, m_lhs.data() + i, sort_a);
+                auto _seq4840_1 = re().mk_concat(all, re().mk_concat(re().mk_to_re(b), all));
+                disj.push_back(re().mk_in_re(_seq4840_0, _seq4840_1));
+            }
             return true;
         }
 
@@ -5134,8 +5238,12 @@ bool seq_rewriter::reduce_eq_empty(expr* l, expr* r, expr_ref& result) {
     }
     // at(s, offset) = "" <=> len(s) <= offset or offset < 0
     if (str().is_at(r, s, offset)) {
-        expr_ref len_s(str().mk_length(s), m()); 
-        result = m().mk_or(m_autil.mk_le(len_s, offset), m_autil.mk_lt(offset, zero()));
+        expr_ref len_s(str().mk_length(s), m());
+        {
+            auto _seq5138_0 = m_autil.mk_le(len_s, offset);
+            auto _seq5138_1 = m_autil.mk_lt(offset, zero());
+            result = m().mk_or(_seq5138_0, _seq5138_1);
+        }
         return true;
     }
     return false;
diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp
index fcba3a8d03..d276ad88e5 100644
--- a/src/ast/rewriter/seq_split.cpp
+++ b/src/ast/rewriter/seq_split.cpp
@@ -313,7 +313,11 @@ expr_ref seq_split::expand_fromre(expr* r, bool& ok) {
     if (rex.is_full_char(r) || rex.is_range(r) || rex.is_of_pred(r)) {
         const expr_ref ex(r, m);
         const expr_ref eps(rex.mk_epsilon(seq_sort), m);
-        return mk_union(mk_single(eps, ex), mk_single(ex, eps));
+        {
+            auto _seq316_0 = mk_single(eps, ex);
+            auto _seq316_1 = mk_single(ex, eps);
+            return mk_union(_seq316_0, _seq316_1);
+        }
     }
 
     // .* : sigma(.*) = { <.*, .*> }
@@ -391,8 +395,11 @@ expr_ref seq_split::expand_fromre(expr* r, bool& ok) {
         return mk_compl(mk_fromre(a));
 
     // difference: a \ b = a & ~b ; sigma(a \ b) = sigma(a) cap ~sigma(b).
-    if (rex.is_diff(r, a, b))
-        return mk_inter(mk_fromre(a), mk_compl(mk_fromre(b)));
+    if (rex.is_diff(r, a, b)) {
+        auto _seq0 = mk_fromre(a);
+        auto _seq1 = mk_compl(mk_fromre(b));
+        return mk_inter(_seq0, _seq1);
+    }
 
     // bounded loop / ite / other: not handled (paper "v1: bail").
     TRACE(seq, tout << "seq_split: unsupported regex " << mk_pp(r, m) << "\n";);
@@ -407,8 +414,11 @@ expr_ref seq_split::distribute_lcat(expr* r, expr* hs) {
         return mk_empty();
     if (is_single(hs, d, n))
         return mk_single(m_rw.mk_re_append(r, d), n);   // r.D
-    if (is_union(hs, a, b))
-        return mk_union(mk_lcat(r, a), mk_lcat(r, b));
+    if (is_union(hs, a, b)) {
+        auto _seq0 = mk_lcat(r, a);
+        auto _seq1 = mk_lcat(r, b);
+        return mk_union(_seq0, _seq1);
+    }
     UNREACHABLE();
     return expr_ref(hs, m);
 }
@@ -420,8 +430,11 @@ expr_ref seq_split::distribute_rcat(expr* hs, expr* r) {
         return mk_empty();
     if (is_single(hs, d, n))
         return mk_single(d, m_rw.mk_re_append(n, r));    // N.r
-    if (is_union(hs, a, b))
-        return mk_union(mk_rcat(a, r), mk_rcat(b, r));
+    if (is_union(hs, a, b)) {
+        auto _seq0 = mk_rcat(a, r);
+        auto _seq1 = mk_rcat(b, r);
+        return mk_union(_seq0, _seq1);
+    }
     UNREACHABLE();
     return expr_ref(hs, m);
 }
diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index 2e1fdfcf7f..4e17bba4a4 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -148,11 +148,19 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         expr * x;
         unsigned val;
         if (m_bv_rw.is_eq_bit(lhs, x, val)) {
-            result = m().mk_eq(x, m().mk_ite(rhs, m_bv_rw.mk_numeral(val, 1), m_bv_rw.mk_numeral(1-val, 1)));
+            {
+                auto _seq151_0 = m_bv_rw.mk_numeral(val, 1);
+                auto _seq151_1 = m_bv_rw.mk_numeral(1 - val, 1);
+                result = m().mk_eq(x, m().mk_ite(rhs, _seq151_0, _seq151_1));
+            }
             return BR_REWRITE2;
         }
         if (m_bv_rw.is_eq_bit(rhs, x, val)) {
-            result = m().mk_eq(x, m().mk_ite(lhs, m_bv_rw.mk_numeral(val, 1), m_bv_rw.mk_numeral(1-val, 1)));
+            {
+                auto _seq155_0 = m_bv_rw.mk_numeral(val, 1);
+                auto _seq155_1 = m_bv_rw.mk_numeral(1 - val, 1);
+                result = m().mk_eq(x, m().mk_ite(lhs, _seq155_0, _seq155_1));
+            }
             return BR_REWRITE2;
         }
         return BR_FAILED;
@@ -253,22 +261,28 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     template<bool SWAP>
     br_status pull_ite_core(func_decl * p, app * ite, app * value, expr_ref & result) {
         if (m().is_eq(p)) {
-            result = m().mk_ite(ite->get_arg(0),
-                                mk_eq_value(ite->get_arg(1), value),
-                                mk_eq_value(ite->get_arg(2), value));
+            {
+                auto _seq256_0 = mk_eq_value(ite->get_arg(1), value);
+                auto _seq256_1 = mk_eq_value(ite->get_arg(2), value);
+                result = m().mk_ite(ite->get_arg(0), _seq256_0, _seq256_1);
+            }
             return BR_REWRITE2;
         }
         else {
             if (SWAP) {
-                result = m().mk_ite(ite->get_arg(0),
-                                    m().mk_app(p, value, ite->get_arg(1)),
-                                    m().mk_app(p, value, ite->get_arg(2)));
+                {
+                    auto _seq263_0 = m().mk_app(p, value, ite->get_arg(1));
+                    auto _seq263_1 = m().mk_app(p, value, ite->get_arg(2));
+                    result = m().mk_ite(ite->get_arg(0), _seq263_0, _seq263_1);
+                }
                 return BR_REWRITE2;
             }
             else {
-                result = m().mk_ite(ite->get_arg(0),
-                                    m().mk_app(p, ite->get_arg(1), value),
-                                    m().mk_app(p, ite->get_arg(2), value));
+                {
+                    auto _seq269_0 = m().mk_app(p, ite->get_arg(1), value);
+                    auto _seq269_1 = m().mk_app(p, ite->get_arg(2), value);
+                    result = m().mk_ite(ite->get_arg(0), _seq269_0, _seq269_1);
+                }
                 return BR_REWRITE2;
             }
         }
@@ -311,10 +325,11 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
                 if (m().is_value(args[1]) && args[0]->get_ref_count() == 1) 
                     return pull_ite_core<false>(f, to_app(args[0]), to_app(args[1]), result);
                 if (m().is_ite(args[1]) && to_app(args[0])->get_arg(0) == to_app(args[1])->get_arg(0)) {
-                    // (p (ite C A1 B1) (ite C A2 B2)) --> (ite (p A1 A2) (p B1 B2))
-                    result = m().mk_ite(to_app(args[0])->get_arg(0),
-                                        m().mk_app(f, to_app(args[0])->get_arg(1), to_app(args[1])->get_arg(1)),
-                                        m().mk_app(f, to_app(args[0])->get_arg(2), to_app(args[1])->get_arg(2)));
+                    {
+                        auto _seq315_0 = m().mk_app(f, to_app(args[0])->get_arg(1), to_app(args[1])->get_arg(1));
+                        auto _seq315_1 = m().mk_app(f, to_app(args[0])->get_arg(2), to_app(args[1])->get_arg(2));
+                        result = m().mk_ite(to_app(args[0])->get_arg(0), _seq315_0, _seq315_1);
+                    }
                     return BR_REWRITE2;
                 }
             }
diff --git a/src/ast/simplifiers/eliminate_predicates.cpp b/src/ast/simplifiers/eliminate_predicates.cpp
index 2fb9b62d8b..1b79a867ed 100644
--- a/src/ast/simplifiers/eliminate_predicates.cpp
+++ b/src/ast/simplifiers/eliminate_predicates.cpp
@@ -207,7 +207,11 @@ void eliminate_predicates::insert_quasi_macro(app* head, expr* body, clause& cl)
     f1 = m.mk_fresh_func_decl(f->get_name(), symbol::null, sorts.size(), sorts.data(), f->get_range());
 
     lhs = m.mk_app(f, args);
-    rhs = m.mk_ite(mk_and(eqs), body, m.mk_app(f1, args));
+    {
+        auto _seq210_0 = mk_and(eqs);
+        auto _seq210_1 = m.mk_app(f1, args);
+        rhs = m.mk_ite(_seq210_0, body, _seq210_1);
+    }
     insert_macro(lhs, rhs, cl);
 }
 
diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp
index 9bbf5bbb3f..0db05f4058 100644
--- a/src/ast/simplifiers/euf_completion.cpp
+++ b/src/ast/simplifiers/euf_completion.cpp
@@ -987,16 +987,23 @@ namespace euf {
                 r = expr_ref(m.mk_true(), m);
             else if (x == x1 && y == y1)
                 r = m_rewriter.mk_eq(x, y);
-            else if (is_nullary(x) && is_nullary(y)) 
-                r = mk_and(m_rewriter.mk_eq(x, x1), m_rewriter.mk_eq(y, x1));
-            else if (x == x1 && is_nullary(x))
+            else if (is_nullary(x) && is_nullary(y)) {
+                auto _seq0 = m_rewriter.mk_eq(x, x1);
+                auto _seq1 = m_rewriter.mk_eq(y, x1);
+                r = mk_and(_seq0, _seq1);
+            } else if (x == x1 && is_nullary(x))
                 r = m_rewriter.mk_eq(y1, x1);
             else if (y == y1 && is_nullary(y))
                 r = m_rewriter.mk_eq(x1, y1);
-            else if (is_nullary(x))
-                r = mk_and(m_rewriter.mk_eq(x, x1), m_rewriter.mk_eq(y1, x1));
-            else if (is_nullary(y))
-                r = mk_and(m_rewriter.mk_eq(y, y1), m_rewriter.mk_eq(x1, y1));
+            else if (is_nullary(x)) {
+                auto _seq0 = m_rewriter.mk_eq(x, x1);
+                auto _seq1 = m_rewriter.mk_eq(y1, x1);
+                r = mk_and(_seq0, _seq1);
+            } else if (is_nullary(y)) {
+                auto _seq0 = m_rewriter.mk_eq(y, y1);
+                auto _seq1 = m_rewriter.mk_eq(x1, y1);
+                r = mk_and(_seq0, _seq1);
+            }
             if (x1 == y1)
                 r = expr_ref(m.mk_true(), m);
             else {
@@ -1005,8 +1012,11 @@ namespace euf {
                     r = m_rewriter.mk_eq(y1, c);
                 else if (c == y1)
                     r = m_rewriter.mk_eq(x1, c);
-                else
-                    r = mk_and(m_rewriter.mk_eq(x1, c), m_rewriter.mk_eq(y1, c));
+                else {
+                    auto _seq1009_0 = m_rewriter.mk_eq(x1, c);
+                    auto _seq1009_1 = m_rewriter.mk_eq(y1, c);
+                    r = mk_and(_seq1009_0, _seq1009_1);
+                }
             }
 
             if (m.proofs_enabled()) {
diff --git a/src/ast/simplifiers/factor_simplifier.cpp b/src/ast/simplifiers/factor_simplifier.cpp
index f803ccb3f0..3e3e11b81c 100644
--- a/src/ast/simplifiers/factor_simplifier.cpp
+++ b/src/ast/simplifiers/factor_simplifier.cpp
@@ -59,7 +59,11 @@ struct factor_simplifier::rw_cfg : public default_rewriter_cfg {
             m_expr2poly.to_expr(fs[i], true, arg);
             args.push_back(arg);
         }
-        result = m.mk_eq(mk_mul(args.size(), args.data()), mk_zero_for(arg));
+        {
+            auto _seq62_0 = mk_mul(args.size(), args.data());
+            auto _seq62_1 = mk_zero_for(arg);
+            result = m.mk_eq(_seq62_0, _seq62_1);
+        }
     }
 
     // p1^k1 * p2^k2 = 0 --> p1 = 0 or p2 = 0
@@ -151,7 +155,9 @@ struct factor_simplifier::rw_cfg : public default_rewriter_cfg {
             }
         }
         else {
-            args.push_back(m.mk_app(m_util.get_family_id(), k, mk_mul(odd_factors.size(), odd_factors.data()), mk_zero_for(odd_factors[0])));
+            auto _seq154_0 = mk_mul(odd_factors.size(), odd_factors.data());
+            auto _seq154_1 = mk_zero_for(odd_factors[0]);
+            args.push_back(m.mk_app(m_util.get_family_id(), k, _seq154_0, _seq154_1));
         }
         SASSERT(!args.empty());
         if (args.size() == 1)