mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-22 20:32:05 +00:00
Code Activity

disable sat solver when proofs are turned on. Fixes issue #768

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-10-31 23:27:39 +01:00
parent fa1a0aa7ba
commit ba942af5a8
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/opt/opt_context.cpp
View file

@ -42,7 +42,6 @@ Notes:
#include "ast_smt_pp.h" #include "ast_smt_pp.h"
#include "filter_model_converter.h" #include "filter_model_converter.h"
#include "ast_pp_util.h" #include "ast_pp_util.h"
#include "inc_sat_solver.h"
#include "qsat.h" #include "qsat.h"
namespace opt { namespace opt {
@ -595,6 +594,9 @@ namespace opt {
if (opt_params(m_params).priority() == symbol("pareto")) { if (opt_params(m_params).priority() == symbol("pareto")) {
return; return;
} }
if (m.proofs_enabled()) {
return;
}
m_params.set_bool("minimize_core_partial", true); m_params.set_bool("minimize_core_partial", true);
m_params.set_bool("minimize_core", true); m_params.set_bool("minimize_core", true);
m_sat_solver = mk_inc_sat_solver(m, m_params); m_sat_solver = mk_inc_sat_solver(m, m_params);