mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 11:26:21 +00:00
Code Activity

[code-simplifier] Simplify api_ast.cpp by removing unreachable branch and stray comment (#9570)

Browse source 
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>
This commit is contained in:
Copilot 2026-05-19 13:56:17 -07:00 • committed by GitHub
parent 3eb6efa830
commit bc6c38e7d3
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/api/api_ast.cpp
View file

@ -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);
}