From bc6c38e7d3424b88a505cacba4b268d0774d4547 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Tue, 19 May 2026 13:56:17 -0700
Subject: [PATCH] [code-simplifier] Simplify `api_ast.cpp` by removing
 unreachable branch and stray comment (#9570)

This change simplifies recently touched API code in
`src/api/api_ast.cpp` without altering semantics. It removes an
unreachable error path in `Z3_get_index_value` and deletes an empty
comment in `Z3_mk_rec_func_decl`.

- **`Z3_get_index_value`: remove dead branch**
- After validating `a` is non-null and of kind `AST_VAR`, the conversion
to `var*` is already guaranteed by existing AST casting invariants.
- The redundant null-check/error-return branch was removed, leaving a
direct index return.

- **`Z3_mk_rec_func_decl`: remove noise**
  - Deleted a stray empty `//` line.

```cpp
// before
var* va = to_var(_a);
if (va) {
    return va->get_idx();
}
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return 0;

// after
var* va = to_var(_a);
return va->get_idx();
```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/api/api_ast.cpp | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 470449378..d7ea3d3c8 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -129,7 +129,6 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_rec_func_decl(c, s, domain_size, domain, range);
         RESET_ERROR_CODE();
-        // 
         recfun::promise_def def = 
             mk_c(c)->recfun().get_plugin().mk_def(
                 to_symbol(s), domain_size, to_sorts(domain), to_sort(range), false);
@@ -1523,11 +1522,7 @@ extern "C" {
             return 0;
         }
         var* va = to_var(_a);
-        if (va) {
-            return va->get_idx();
-        }
-        SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
-        return 0;
+        return va->get_idx();
         Z3_CATCH_RETURN(0);
     }