From 0ab2067b69d876914a79ae7467db41a698f9a3ca Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Dec 2016 13:15:40 +0100 Subject: [PATCH] produce error message for cores with optimization. Issue #825 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 5 +++++ src/opt/opt_context.h | 2 +- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 624671e2b..b95bb62e8 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -169,6 +169,11 @@ namespace opt { r.append(m_labels); } + void context::get_unsat_core(ptr_vector & r) { + throw default_exception("Unsat cores are not supported with optimization"); + } + + void context::set_hard_constraints(ptr_vector& fmls) { if (m_scoped_state.set(fmls)) { clear_state(); diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 18af756bf..ef02a4cbe 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -190,7 +190,7 @@ namespace opt { virtual void collect_statistics(statistics& stats) const; virtual proof* get_proof() { return 0; } virtual void get_labels(svector & r); - virtual void get_unsat_core(ptr_vector & r) {} + virtual void get_unsat_core(ptr_vector & r); virtual std::string reason_unknown() const; virtual void set_reason_unknown(char const* msg) { m_unknown = msg; }