mirror of
https://github.com/Z3Prover/z3
synced 2025-06-19 20:33:38 +00:00
initialize solver prior to translate. fixes build break
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
5995c753d3
commit
84f935ae85
1 changed files with 1 additions and 0 deletions
|
@ -103,6 +103,7 @@ extern "C" {
|
||||||
RESET_ERROR_CODE();
|
RESET_ERROR_CODE();
|
||||||
params_ref const& p = to_solver(s)->m_params;
|
params_ref const& p = to_solver(s)->m_params;
|
||||||
Z3_solver_ref * sr = alloc(Z3_solver_ref, 0);
|
Z3_solver_ref * sr = alloc(Z3_solver_ref, 0);
|
||||||
|
init_solver(c, s);
|
||||||
sr->m_solver = to_solver(s)->m_solver->translate(mk_c(target)->m(), p);
|
sr->m_solver = to_solver(s)->m_solver->translate(mk_c(target)->m(), p);
|
||||||
mk_c(target)->save_object(sr);
|
mk_c(target)->save_object(sr);
|
||||||
Z3_solver r = of_solver(sr);
|
Z3_solver r = of_solver(sr);
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue