From 14b9dd2cd71c9fb7f2b036fa4aa37e31a3666006 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 24 May 2018 16:25:55 -0700 Subject: [PATCH] spacer: let pool_solver own the solver --- src/muz/spacer/spacer_manager.cpp | 15 +++++++++------ src/muz/spacer/spacer_manager.h | 3 --- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/muz/spacer/spacer_manager.cpp b/src/muz/spacer/spacer_manager.cpp index a281cac81..d55f74b90 100644 --- a/src/muz/spacer/spacer_manager.cpp +++ b/src/muz/spacer/spacer_manager.cpp @@ -179,13 +179,16 @@ static std::vector state_suffixes() { manager::manager(unsigned max_num_contexts, ast_manager& manager) : m(manager), m_mux(m, state_suffixes()) { - m_pool0_base = mk_smt_solver(m, params_ref::get_empty(), symbol::null); - m_pool1_base = mk_smt_solver(m, params_ref::get_empty(), symbol::null); - m_pool2_base = mk_smt_solver(m, params_ref::get_empty(), symbol::null); + ref pool0_base = + mk_smt_solver(m, params_ref::get_empty(), symbol::null); + ref pool1_base = + mk_smt_solver(m, params_ref::get_empty(), symbol::null); + ref pool2_base = + mk_smt_solver(m, params_ref::get_empty(), symbol::null); - m_pool0 = alloc(solver_pool, m_pool0_base.get(), max_num_contexts); - m_pool1 = alloc(solver_pool, m_pool1_base.get(), max_num_contexts); - m_pool2 = alloc(solver_pool, m_pool2_base.get(), max_num_contexts); + m_pool0 = alloc(solver_pool, pool0_base.get(), max_num_contexts); + m_pool1 = alloc(solver_pool, pool1_base.get(), max_num_contexts); + m_pool2 = alloc(solver_pool, pool2_base.get(), max_num_contexts); } diff --git a/src/muz/spacer/spacer_manager.h b/src/muz/spacer/spacer_manager.h index 4c3d861cb..b8783369d 100644 --- a/src/muz/spacer/spacer_manager.h +++ b/src/muz/spacer/spacer_manager.h @@ -79,9 +79,6 @@ class manager { // manager of multiplexed names sym_mux m_mux; - ref m_pool0_base; - ref m_pool1_base; - ref m_pool2_base; // three solver pools for different queries scoped_ptr m_pool0; scoped_ptr m_pool1;