From 5db349f6fafc5b117dd49e11d7f2cd42531732af Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 27 Aug 2017 23:52:27 -0700 Subject: [PATCH] raise an exception if trying proof generation for the SAT solver. Stackoverflow question https://stackoverflow.com/questions/45885321/check-function-while-qf-fd-logic-is-set-throws-accessviolationexception Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 3 +++ src/tactic/portfolio/smt_strategic_solver.cpp | 4 ++-- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 521aa5e71..21f9f1e8a 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -388,6 +388,9 @@ private: m_subgoals.reset(); init_preprocess(); SASSERT(g->models_enabled()); + if (g->proofs_enabled()) { + throw default_exception("generation of proof objects is not supported in this mode"); + } SASSERT(!g->proofs_enabled()); TRACE("sat", g->display(tout);); try { diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 0ad9e5f19..3e77b7abc 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -93,7 +93,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const return mk_qffpbv_tactic(m, p); else if (logic=="HORN") return mk_horn_tactic(m, p); - else if (logic == "QF_FD" || logic == "SAT") + else if ((logic == "QF_FD" || logic == "SAT") && !m.proofs_enabled()) return mk_solver2tactic(mk_fd_solver(m, p)); //else if (logic=="QF_UFNRA") // return mk_qfufnra_tactic(m, p); @@ -102,7 +102,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const } static solver* mk_special_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) { - if (logic == "QF_FD" || logic == "SAT") + if ((logic == "QF_FD" || logic == "SAT") && !m.proofs_enabled()) return mk_fd_solver(m, p); return 0; }