From d86e8f02d7808fed783a5eedc4d8f5255008c6f4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Dec 2017 10:09:10 -0800 Subject: [PATCH] fix get-objectives error #1419 message (get-objectives) Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 3d296d92b..0daf98320 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1235,6 +1235,9 @@ namespace opt { } void context::display_assignment(std::ostream& out) { + if (m_scoped_state.m_objectives.size() != m_objectives.size()) { + throw default_exception("check-sat has not been called with latest objectives"); + } out << "(objectives\n"; for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) { objective const& obj = m_scoped_state.m_objectives[i];