From cfd00ad672dbe1334976c35867001e3f96f63692 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Oct 2024 09:22:23 -0700 Subject: [PATCH] add slice solver option to command context --- src/cmd_context/cmd_context.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 59de003c86..577cc95b62 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -51,6 +51,7 @@ Module Name: #include "solver/smt_logics.h" #include "cmd_context/basic_cmds.h" #include "cmd_context/cmd_context.h" +#include "solver/slice_solver.h" #include func_decls::func_decls(ast_manager & m, func_decl * f): @@ -2257,6 +2258,7 @@ void cmd_context::mk_solver() { params_ref p; 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 = mk_slice_solver(m_solver.get()); }