From 56f4d5a68e6c5464e7c3ca4e0b5a2f84096848c4 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
 <41898282+github-actions[bot]@users.noreply.github.com>
Date: Wed, 27 May 2026 05:50:58 +0000
Subject: [PATCH] smt2parser: fix indentation in pop_app_frame else block

The else branch added in #9636 for the non-expr_head path was
missing indentation, making the code hard to read and inconsistent
with the surrounding style. Also removes trailing whitespace on
two mk_app call lines.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 src/parsers/smt2/smt2parser.cpp | 46 ++++++++++++++++-----------------
 1 file changed, 23 insertions(+), 23 deletions(-)

diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 6d1f3a4f20..0c214e99a2 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -1998,32 +1998,32 @@ namespace smt2 {
                 }
             }
             else {
-            local l;
-            if (m_env.find(fr->m_f, l)) {
-                push_local(l);
-                t_ref = expr_stack().back();
-                for (unsigned i = 0; i < num_args; ++i) {
-                    expr* arg = expr_stack().get(fr->m_expr_spos + i);
-                    expr* args[2] = { t_ref.get(), arg };
-                    m_ctx.mk_app(symbol("select"), 
-                                 2, 
-                                 args,
-                                 0,
-                                 nullptr,
-                                 nullptr,
+                local l;
+                if (m_env.find(fr->m_f, l)) {
+                    push_local(l);
+                    t_ref = expr_stack().back();
+                    for (unsigned i = 0; i < num_args; ++i) {
+                        expr* arg = expr_stack().get(fr->m_expr_spos + i);
+                        expr* args[2] = { t_ref.get(), arg };
+                        m_ctx.mk_app(symbol("select"),
+                                     2,
+                                     args,
+                                     0,
+                                     nullptr,
+                                     nullptr,
+                                     t_ref);
+                    }
+                }
+                else {
+                    m_ctx.mk_app(fr->m_f,
+                                 num_args,
+                                 expr_stack().data() + fr->m_expr_spos,
+                                 num_indices,
+                                 m_param_stack.data() + fr->m_param_spos,
+                                 fr->m_as_sort ? sort_stack().back() : nullptr,
                                  t_ref);
                 }
             }
-            else {
-                m_ctx.mk_app(fr->m_f,
-                             num_args,
-                             expr_stack().data() + fr->m_expr_spos,
-                             num_indices,
-                             m_param_stack.data() + fr->m_param_spos,
-                             fr->m_as_sort ? sort_stack().back() : nullptr,
-                             t_ref);
-            }
-            }
             expr_stack().shrink(fr->m_expr_spos);
             m_param_stack.shrink(fr->m_param_spos);
             if (fr->m_as_sort)