From 1681419052d156240b76c4e85b5750b82ecc6a88 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 23 Jun 2017 16:50:33 -0700 Subject: [PATCH] adding change notes to release notes for a future release Signed-off-by: Nikolaj Bjorner --- RELEASE_NOTES | 10 ++++++++++ src/smt/smt_context.cpp | 8 +++++--- 2 files changed, 15 insertions(+), 3 deletions(-) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 357c17e78..ec05160da 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -1,5 +1,15 @@ RELEASE NOTES +Version 4.5.x +============= +- New features (including): + - A new string solver from University of Waterloo + - A new linear real arithmetic solver + - Changed behavior for optimization commands from the SMT2 command-line interface. + Objective values are no longer printed by default. They can be retrieved by + issuing the command (get-objectives). Pareto front objectives are accessed by + issuing multiple (check-sat) calls until it returns unsat. + Version 4.5.0 ============= diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 0c32f3c76..4e56d3004 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4332,10 +4332,9 @@ namespace smt { ); failure fl = get_last_search_failure(); if (fl == MEMOUT || fl == CANCELED || fl == TIMEOUT || fl == NUM_CONFLICTS || fl == RESOURCE_LIMIT) { - return; + TRACE("get_model", tout << "last search failure: " << fl << "\n";); } - - if (m_fparams.m_model || m_fparams.m_model_on_final_check || m_qmanager->model_based()) { + else if (m_fparams.m_model || m_fparams.m_model_on_final_check || m_qmanager->model_based()) { m_model_generator->reset(); m_proto_model = m_model_generator->mk_model(); m_qmanager->adjust_model(m_proto_model.get()); @@ -4346,6 +4345,9 @@ namespace smt { if (m_fparams.m_model_compact) m_proto_model->compress(); TRACE("mbqi_bug", tout << "after cleanup:\n"; model_pp(tout, *m_proto_model);); + } + else { + } }