From 424f34d3d948283b61c92f089cc3b90e76c44324 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 11 Aug 2015 11:16:41 +0200 Subject: [PATCH] enable smt tactic to be used even if cores are enabled, as long as no cores are tracked, fixes issue #189 Signed-off-by: Nikolaj Bjorner --- src/smt/tactic/smt_tactic.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 2d9a8fb82..c441a7d45 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -210,9 +210,9 @@ public: ptr_vector assumptions; ref fmc; if (in->unsat_core_enabled()) { - if (in->proofs_enabled()) - throw tactic_exception("smt tactic does not support simultaneous generation of proofs and unsat cores"); extract_clauses_and_dependencies(in, clauses, assumptions, bool2dep, fmc); + if (in->proofs_enabled() && !assumptions.empty()) + throw tactic_exception("smt tactic does not support simultaneous generation of proofs and unsat cores"); for (unsigned i = 0; i < clauses.size(); ++i) { m_ctx->assert_expr(clauses[i].get()); }