From 650e2a4e5aedda4bdf5592f00b99471c0087ff7a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
Date: Wed, 5 Aug 2026 09:00:28 -0700
Subject: [PATCH] [code-simplifier] seq_monadic_bench: replace comma-operator
 chains with explicit statements (#10408)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

…ents

Replace confusing comma-operator idioms with clear, explicit
multi-statement code:

- parse_guard: replace comma-chained return with braced blocks
- lo/hi accumulation: replace comma one-liners with separate statements
- collect lambda: replace comma-combined complete/dropped updates

No functional change; behavior is identical.

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 src/test/seq_monadic_bench.cpp | 30 +++++++++++++++++++-----------
 1 file changed, 19 insertions(+), 11 deletions(-)

diff --git a/src/test/seq_monadic_bench.cpp b/src/test/seq_monadic_bench.cpp
index 1c28e81ec8..ddb3908460 100644
--- a/src/test/seq_monadic_bench.cpp
+++ b/src/test/seq_monadic_bench.cpp
@@ -260,10 +260,12 @@ lbool run_file(
             else if (a.is_gt(e, rhs, lhs)) strict = true;
             else return false;
             rational v;
-            if (is_int_var(lhs) && a.is_numeral(rhs, v))
-                return k = lhs, is_lower = false, bound = strict ? v - 1 : v, true;
-            if (a.is_numeral(lhs, v) && is_int_var(rhs))
-                return k = rhs, is_lower = true, bound = strict ? v + 1 : v, true;
+            if (is_int_var(lhs) && a.is_numeral(rhs, v)) {
+                k = lhs; is_lower = false; bound = strict ? v - 1 : v; return true;
+            }
+            if (a.is_numeral(lhs, v) && is_int_var(rhs)) {
+                k = rhs; is_lower = true; bound = strict ? v + 1 : v; return true;
+            }
             return false;
         };
 
@@ -302,10 +304,13 @@ lbool run_file(
                     ok = false;
                     break;
                 }
-                if (is_lower)
-                    lo = has_lo ? std::max(lo, bound) : bound, has_lo = true;
-                else
-                    hi = has_hi ? std::min(hi, bound) : bound, has_hi = true;
+                if (is_lower) {
+                    lo = has_lo ? std::max(lo, bound) : bound;
+                    has_lo = true;
+                } else {
+                    hi = has_hi ? std::min(hi, bound) : bound;
+                    has_hi = true;
+                }
                 guards.push_back(other);
             }
             if (!ok)
@@ -374,13 +379,16 @@ lbool run_file(
         else if (m.is_not(e, arg) && u.str.is_in_re(arg, s, r))
             negated = true;
         else if (!u.str.is_in_re(e, s, r)) {
-            if (!collect_len(e, false))
-                complete = false, ++dropped;
+            if (!collect_len(e, false)) {
+                complete = false;
+                ++dropped;
+            }
             return;
         }
         bool is_var = is_seq_var(s);
         if (!is_var && !u.str.is_concat(s)) {
-            complete = false, ++dropped;
+            complete = false;
+            ++dropped;
             return;
         }
         obj_map<expr, expr*>& map = is_var ? var_re : term_re;