From b6400e8e3d73f69b2a883b1a3d91ca0efd6a2bb7 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
 <41898282+github-actions[bot]@users.noreply.github.com>
Date: Tue, 19 May 2026 05:41:39 +0000
Subject: [PATCH] simplify api_ast.cpp: remove dead code and empty comment

- Z3_get_index_value: remove redundant null check on 'va'; after verifying
  _a->get_kind() == AST_VAR, to_var(_a) always returns a valid pointer,
  so the 'if (va)' branch and its error-handling were unreachable dead code.
- Z3_mk_rec_func_decl: remove empty comment line ('//').

Co-authored-by: Copilot <223556219+Copilot@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);
     }