From 86c39c971d12be7e063e05d26582a53e7f10194a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Jun 2018 21:53:45 -0700 Subject: [PATCH] fix #1681 Signed-off-by: Nikolaj Bjorner --- src/smt/proto_model/proto_model.cpp | 16 +++++++++++----- src/smt/proto_model/proto_model.h | 4 ++-- src/smt/smt_context.cpp | 2 +- src/smt/smt_model_finder.cpp | 2 +- 4 files changed, 15 insertions(+), 9 deletions(-) diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index 688ded834..493948f32 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -342,10 +342,16 @@ void proto_model::compress() { \brief Complete the interpretation fi of f if it is partial. If f does not have an interpretation in the given model, then this is a noop. */ -void proto_model::complete_partial_func(func_decl * f) { +void proto_model::complete_partial_func(func_decl * f, bool use_fresh) { func_interp * fi = get_func_interp(f); if (fi && fi->is_partial()) { - expr * else_value = fi->get_max_occ_result(); + expr * else_value; + if (use_fresh) { + else_value = get_fresh_value(f->get_range()); + } + else { + else_value = fi->get_max_occ_result(); + } if (else_value == nullptr) else_value = get_some_value(f->get_range()); fi->set_else(else_value); @@ -355,14 +361,14 @@ void proto_model::complete_partial_func(func_decl * f) { /** \brief Set the (else) field of function interpretations... */ -void proto_model::complete_partial_funcs() { +void proto_model::complete_partial_funcs(bool use_fresh) { if (m_model_partial) return; // m_func_decls may be "expanded" when we invoke get_some_value. // So, we must not use iterators to traverse it. - for (unsigned i = 0; i < m_func_decls.size(); i++) { - complete_partial_func(m_func_decls[i]); + for (func_decl* f : m_func_decls) { + complete_partial_func(f, use_fresh); } } diff --git a/src/smt/proto_model/proto_model.h b/src/smt/proto_model/proto_model.h index d92d459e4..04e3a90fe 100644 --- a/src/smt/proto_model/proto_model.h +++ b/src/smt/proto_model/proto_model.h @@ -100,8 +100,8 @@ public: // // Complete partial function interps // - void complete_partial_func(func_decl * f); - void complete_partial_funcs(); + void complete_partial_func(func_decl * f, bool use_fresh); + void complete_partial_funcs(bool use_fresh); // // Create final model object. diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index b2adfff8d..48033f9b5 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4364,7 +4364,7 @@ namespace smt { m_proto_model = m_model_generator->mk_model(); m_qmanager->adjust_model(m_proto_model.get()); TRACE("mbqi_bug", tout << "before complete_partial_funcs:\n"; model_pp(tout, *m_proto_model);); - m_proto_model->complete_partial_funcs(); + m_proto_model->complete_partial_funcs(false); TRACE("mbqi_bug", tout << "before cleanup:\n"; model_pp(tout, *m_proto_model);); m_proto_model->cleanup(); if (m_fparams.m_model_compact) diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 4307d3fdf..73f85faf6 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -1028,7 +1028,7 @@ namespace smt { void complete_partial_funcs(func_decl_set const & partial_funcs) { for (func_decl * f : partial_funcs) { // Complete the current interpretation - m_model->complete_partial_func(f); + m_model->complete_partial_func(f, true); unsigned arity = f->get_arity(); func_interp * fi = m_model->get_func_interp(f);