From e6c082e6e888edca3738d2dd52c93df0e60e122d Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 12 Mar 2026 22:19:41 +0000 Subject: [PATCH 1/3] Initial plan From f413a24408b800b60e1cb544a45a3106041199dc Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 12 Mar 2026 22:58:53 +0000 Subject: [PATCH 2/3] Fix API bugs exercised by test/deep_api_bugs.cpp - api_fpa.cpp: add RETURN_Z3(nullptr) after SET_ERROR_CODE in Z3_mk_fpa_sort to prevent fall-through to mk_float_sort with invalid params - api_seq.cpp: add null check for str in Z3_mk_string; add null check for str when sz>0 in Z3_mk_lstring; add lo<=hi validation in Z3_mk_re_loop - api_array.cpp: add explicit n==0 validation in Z3_mk_array_sort_n - api_solver.cpp: rename local variable 'c' to avoid shadowing Z3_context param in Z3_solver_propagate_created/decide/on_binding; move init_solver call inside file-exists branches of Z3_solver_from_file - api_ast.cpp: add null check for target in Z3_translate; add null check for _from/_to arrays when num_exprs>0 in Z3_substitute - api_model.cpp: add CHECK_NON_NULL(m) in Z3_add_func_interp; add CHECK_NON_NULL(a) in Z3_model_get_const_interp; add null check for target in Z3_model_translate - api_opt.cpp: add null check for weight string in Z3_optimize_assert_soft - api_quant.cpp: add num_patterns==0 validation in Z3_mk_pattern Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/api/api_array.cpp | 4 ++++ src/api/api_ast.cpp | 8 ++++++++ src/api/api_fpa.cpp | 1 + src/api/api_model.cpp | 6 ++++++ src/api/api_opt.cpp | 6 +++++- src/api/api_quant.cpp | 4 ++++ src/api/api_seq.cpp | 12 ++++++++++++ src/api/api_solver.cpp | 15 ++++++++------- 8 files changed, 48 insertions(+), 8 deletions(-) diff --git a/src/api/api_array.cpp b/src/api/api_array.cpp index e0f71f2b7..e01248b31 100644 --- a/src/api/api_array.cpp +++ b/src/api/api_array.cpp @@ -38,6 +38,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_array_sort_n(c, n, domain, range); RESET_ERROR_CODE(); + if (n == 0) { + SET_ERROR_CODE(Z3_INVALID_ARG, "array sort requires at least one domain sort"); + RETURN_Z3(nullptr); + } vector params; for (unsigned i = 0; i < n; ++i) params.push_back(parameter(to_sort(domain[i]))); params.push_back(parameter(to_sort(range))); diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 69ac1303f..c0dd3c837 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -898,6 +898,10 @@ extern "C" { RESET_ERROR_CODE(); ast_manager & m = mk_c(c)->m(); expr * a = to_expr(_a); + if (num_exprs > 0 && (!_from || !_to)) { + SET_ERROR_CODE(Z3_INVALID_ARG, "null from/to arrays with non-zero num_exprs"); + RETURN_Z3(of_expr(nullptr)); + } expr * const * from = to_exprs(num_exprs, _from); expr * const * to = to_exprs(num_exprs, _to); expr * r = nullptr; @@ -1514,6 +1518,10 @@ extern "C" { LOG_Z3_translate(c, a, target); RESET_ERROR_CODE(); CHECK_VALID_AST(a, nullptr); + if (!target) { + SET_ERROR_CODE(Z3_INVALID_ARG, "null target context"); + RETURN_Z3(nullptr); + } if (c == target) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index c0cfcd079..aeeb24c41 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -167,6 +167,7 @@ extern "C" { RESET_ERROR_CODE(); if (ebits < 2 || sbits < 3) { SET_ERROR_CODE(Z3_INVALID_ARG, "ebits should be at least 2, sbits at least 3"); + RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); sort * s = ctx->fpautil().mk_float_sort(ebits, sbits); diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index 18f6bf578..bfd6561a2 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -64,6 +64,7 @@ extern "C" { LOG_Z3_model_get_const_interp(c, m, a); RESET_ERROR_CODE(); CHECK_NON_NULL(m, nullptr); + CHECK_NON_NULL(a, nullptr); expr * r = to_model_ref(m)->get_const_interp(to_func_decl(a)); if (!r) { RETURN_Z3(nullptr); @@ -212,6 +213,10 @@ extern "C" { Z3_TRY; LOG_Z3_model_translate(c, m, target); RESET_ERROR_CODE(); + if (!target) { + SET_ERROR_CODE(Z3_INVALID_ARG, "null target context"); + RETURN_Z3(nullptr); + } Z3_model_ref* dst = alloc(Z3_model_ref, *mk_c(target)); ast_translation tr(mk_c(c)->m(), mk_c(target)->m()); dst->m_model = to_model_ref(m)->translate(tr); @@ -246,6 +251,7 @@ extern "C" { Z3_TRY; LOG_Z3_add_func_interp(c, m, f, else_val); RESET_ERROR_CODE(); + CHECK_NON_NULL(m, nullptr); CHECK_NON_NULL(f, nullptr); func_decl* d = to_func_decl(f); model* mdl = to_model_ref(m); diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index 68c4844c3..bf8fc9871 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -94,7 +94,11 @@ extern "C" { Z3_TRY; LOG_Z3_optimize_assert_soft(c, o, a, weight, id); RESET_ERROR_CODE(); - CHECK_FORMULA(a,0); + CHECK_FORMULA(a,0); + if (!weight) { + SET_ERROR_CODE(Z3_INVALID_ARG, "null weight string"); + return 0; + } rational w(weight); return to_optimize_ptr(o)->add_soft_constraint(to_expr(a), w, to_symbol(id)); Z3_CATCH_RETURN(0); diff --git a/src/api/api_quant.cpp b/src/api/api_quant.cpp index c495f253e..83e2fa593 100644 --- a/src/api/api_quant.cpp +++ b/src/api/api_quant.cpp @@ -321,6 +321,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_pattern(c, num_patterns, terms); RESET_ERROR_CODE(); + if (num_patterns == 0) { + SET_ERROR_CODE(Z3_INVALID_ARG, "pattern requires at least one term"); + RETURN_Z3(nullptr); + } for (unsigned i = 0; i < num_patterns; ++i) { if (!is_app(to_expr(terms[i]))) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index cf199af41..4ceb82739 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -48,6 +48,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_string(c, str); RESET_ERROR_CODE(); + if (!str) { + SET_ERROR_CODE(Z3_INVALID_ARG, "null string"); + RETURN_Z3(nullptr); + } zstring s(str); app* a = mk_c(c)->sutil().str.mk_string(s); mk_c(c)->save_ast_trail(a); @@ -59,6 +63,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_lstring(c, sz, str); RESET_ERROR_CODE(); + if (sz > 0 && !str) { + SET_ERROR_CODE(Z3_INVALID_ARG, "null string buffer"); + RETURN_Z3(nullptr); + } unsigned_vector chs; for (unsigned i = 0; i < sz; ++i) chs.push_back((unsigned char)str[i]); zstring s(sz, chs.data()); @@ -314,6 +322,10 @@ extern "C" { Z3_TRY; LOG_Z3_mk_re_loop(c, r, lo, hi); RESET_ERROR_CODE(); + if (hi != 0 && lo > hi) { + SET_ERROR_CODE(Z3_INVALID_ARG, "loop lower bound must not exceed upper bound"); + RETURN_Z3(nullptr); + } app* a = hi == 0 ? mk_c(c)->sutil().re.mk_loop(to_expr(r), lo) : mk_c(c)->sutil().re.mk_loop(to_expr(r), lo, hi); mk_c(c)->save_ast_trail(a); RETURN_Z3(of_ast(a)); diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 1eb194b71..3da361921 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -379,14 +379,15 @@ extern "C" { LOG_Z3_solver_from_file(c, s, file_name); char const* ext = get_extension(file_name); std::ifstream is(file_name); - init_solver(c, s); if (!is) { SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR, nullptr); } else if (ext && (std::string("dimacs") == ext || std::string("cnf") == ext)) { + init_solver(c, s); solver_from_dimacs_stream(c, s, is); } else { + init_solver(c, s); solver_from_stream(c, s, is); } Z3_CATCH; @@ -1153,24 +1154,24 @@ extern "C" { void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh) { Z3_TRY; RESET_ERROR_CODE(); - user_propagator::created_eh_t c = (void(*)(void*, user_propagator::callback*, expr*))created_eh; - to_solver_ref(s)->user_propagate_register_created(c); + user_propagator::created_eh_t created_fn = (void(*)(void*, user_propagator::callback*, expr*))created_eh; + to_solver_ref(s)->user_propagate_register_created(created_fn); Z3_CATCH; } void Z3_API Z3_solver_propagate_decide(Z3_context c, Z3_solver s, Z3_decide_eh decide_eh) { Z3_TRY; RESET_ERROR_CODE(); - user_propagator::decide_eh_t c = (void(*)(void*, user_propagator::callback*, expr*, unsigned, bool))decide_eh; - to_solver_ref(s)->user_propagate_register_decide(c); + user_propagator::decide_eh_t decide_fn = (void(*)(void*, user_propagator::callback*, expr*, unsigned, bool))decide_eh; + to_solver_ref(s)->user_propagate_register_decide(decide_fn); Z3_CATCH; } void Z3_API Z3_solver_propagate_on_binding(Z3_context c, Z3_solver s, Z3_on_binding_eh binding_eh) { Z3_TRY; RESET_ERROR_CODE(); - user_propagator::binding_eh_t c = (bool(*)(void*, user_propagator::callback*, expr*, expr*))binding_eh; - to_solver_ref(s)->user_propagate_register_on_binding(c); + user_propagator::binding_eh_t binding_fn = (bool(*)(void*, user_propagator::callback*, expr*, expr*))binding_eh; + to_solver_ref(s)->user_propagate_register_on_binding(binding_fn); Z3_CATCH; } From 682fa3f81531991f984ccf4c3a29c00b46439806 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 12 Mar 2026 23:00:07 +0000 Subject: [PATCH 3/3] Fix indentation: use spaces instead of tabs in api_model.cpp CHECK_NON_NULL Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/api/api_model.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index bfd6561a2..3e065fb64 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -252,7 +252,7 @@ extern "C" { LOG_Z3_add_func_interp(c, m, f, else_val); RESET_ERROR_CODE(); CHECK_NON_NULL(m, nullptr); - CHECK_NON_NULL(f, nullptr); + CHECK_NON_NULL(f, nullptr); func_decl* d = to_func_decl(f); model* mdl = to_model_ref(m); Z3_func_interp_ref * f_ref = alloc(Z3_func_interp_ref, *mk_c(c), mdl);