From 1e7832a391d6935aa7356e9e30737ca0a3ae1af0 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Thu, 14 Aug 2025 18:13:23 -0700 Subject: [PATCH] Use solver factory translate method in Z3_solver_translate (#7782) * Initial plan * Fix Z3_solver_translate to use solver factory translate method Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- 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_solver.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index c9ce1f5cc..05b93d38b 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -276,7 +276,11 @@ extern "C" { LOG_Z3_solver_translate(c, s, target); RESET_ERROR_CODE(); params_ref const& p = to_solver(s)->m_params; - Z3_solver_ref * sr = alloc(Z3_solver_ref, *mk_c(target), (solver_factory *)nullptr); + solver_factory* translated_factory = nullptr; + if (to_solver(s)->m_solver_factory.get()) { + translated_factory = to_solver(s)->m_solver_factory->translate(mk_c(target)->m()); + } + Z3_solver_ref * sr = alloc(Z3_solver_ref, *mk_c(target), translated_factory); init_solver(c, s); sr->m_solver = to_solver(s)->m_solver->translate(mk_c(target)->m(), p); mk_c(target)->save_object(sr);