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

simplify api_ast.cpp: remove dead code and empty comment

Browse source 
- 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>
This commit is contained in:
github-actions[bot] 2026-05-19 05:41:39 +00:00 • committed by GitHub
parent d4babf7181
commit b6400e8e3d
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; Z3_TRY;
LOG_Z3_mk_rec_func_decl(c, s, domain_size, domain, range); LOG_Z3_mk_rec_func_decl(c, s, domain_size, domain, range);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
//
recfun::promise_def def = recfun::promise_def def =
mk_c(c)->recfun().get_plugin().mk_def( mk_c(c)->recfun().get_plugin().mk_def(
to_symbol(s), domain_size, to_sorts(domain), to_sort(range), false); to_symbol(s), domain_size, to_sorts(domain), to_sort(range), false);
@ -1523,11 +1522,7 @@ extern "C" {
return 0; return 0;
} }
var* va = to_var(_a); var* va = to_var(_a);
if (va) { return va->get_idx();
return va->get_idx();
}
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return 0;
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }