From 7d545d902df1cace6e09694132e54daaa9c3cf40 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 Jul 2016 17:36:11 -0700 Subject: [PATCH] switch to specialized consequence generator in combined_solver Signed-off-by: Nikolaj Bjorner --- src/solver/combined_solver.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index 7db056396..30b387b98 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -194,6 +194,11 @@ public: return m_solver1->get_scope_level(); } + virtual lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { + switch_inc_mode(); + return m_solver2->get_consequences(asms, vars, consequences); + } + virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) { m_check_sat_executed = true; m_use_solver1_results = false;