mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

add slice solver option to command context

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-10-08 09:22:23 -07:00
parent 8a95dd4d65
commit cfd00ad672
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/cmd_context/cmd_context.cpp
View file

@ -51,6 +51,7 @@ Notes:
#include "solver/smt_logics.h" #include "solver/smt_logics.h"
#include "cmd_context/basic_cmds.h" #include "cmd_context/basic_cmds.h"
#include "cmd_context/cmd_context.h" #include "cmd_context/cmd_context.h"
#include "solver/slice_solver.h"
#include <iostream> #include <iostream>
func_decls::func_decls(ast_manager & m, func_decl * f): func_decls::func_decls(ast_manager & m, func_decl * f):
@ -2257,6 +2258,7 @@ void cmd_context::mk_solver() {
params_ref p; params_ref p;
m_params.get_solver_params(p, proofs_enabled, models_enabled, unsat_core_enabled); m_params.get_solver_params(p, proofs_enabled, models_enabled, unsat_core_enabled);
m_solver = (*m_solver_factory)(m(), p, proofs_enabled, models_enabled, unsat_core_enabled, m_logic); m_solver = (*m_solver_factory)(m(), p, proofs_enabled, models_enabled, unsat_core_enabled, m_logic);
m_solver = mk_slice_solver(m_solver.get());
} }