[code-simplifier] smt2parser: fix indentation in pop_app_frame else block

[github-actions]

Code Simplification - 2026-05-27

This PR fixes an indentation issue introduced in #9636 to improve code clarity and consistency without changing any behavior.

Files Simplified

• src/parsers/smt2/smt2parser.cpp — Fixed indentation of the else block in pop_app_frame and removed trailing whitespace

Improvements Made

Fixed Indentation in pop_app_frame

The else block added in #9636 for the non-expr_head path had its body at the same indentation level as the else keyword itself, making the nested if/else structure visually ambiguous:

// Before (confusing — body not indented inside else)
else {
local l;
if (m_env.find(fr->m_f, l)) {
    ...
}
else {
    ...
}
}

// After (clear structure)
else {
    local l;
    if (m_env.find(fr->m_f, l)) {
        ...
    }
    else {
        ...
    }
}

Also removed two trailing spaces on mk_app call lines within the same block.

Changes Based On

Recent changes from:

• SMT2 front-end: accept HO_ALL and normalize curried expression-head applications #9636 - SMT2 front-end: accept HO_ALL and normalize curried expression-head applications

Testing

• ✅ No functional changes — whitespace/indentation only
• ✅ Behavior is identical

---

Automated by Code Simplifier Agent - analyzing code from the last 24 hours

Note

🔒 Integrity filter blocked 2 items

The following items were blocked because they don't meet the GitHub integrity level.

• #9628 search_pull_requests: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".
• #9597 search_pull_requests: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".

To allow these resources, lower min-integrity in your GitHub frontmatter:

tools:
  github:
    min-integrity: approved  # merged | approved | unapproved | none

Generated by Code Simplifier · sonnet46 1M · ◷

Add this agentic workflows to your repo

To install this agentic workflow, run

gh aw add github/gh-aw/.github/workflows/code-simplifier.md@6762bfba6ae426a03aac46e8f68701461c667404

• expires on May 28, 2026, 5:50 AM UTC

---

Note

This was originally intended as a pull request, but GitHub Actions is not permitted to create or approve pull requests in this repository.
The changes have been pushed to branch code-simplifier/fix-pop-app-frame-indentation-d94e72b433144153.

Click here to create the pull request

To fix the permissions issue, go to Settings → Actions → General and enable Allow GitHub Actions to create and approve pull requests. See also: gh-aw FAQ

Show patch preview (79 of 79 lines)

From d301dd4dfb3c45dda991ccbecc3cec540123d73b Mon Sep 17 00:00:00 2001
From: "github-actions[bot]" <github-actions[bot]@users.noreply.github.com>
Date: Wed, 27 May 2026 05:47:23 +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 6d1f3a4..0c214e9 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,
+  
... (truncated)