From 6780784bcff98715450c73ef43791d642e817052 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Aug 2015 14:43:08 +0200 Subject: [PATCH] filter instantiations for model values to fix issue #183 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_model_checker.cpp | 6 ++---- src/smt/smt_model_finder.cpp | 1 + 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 9c20c5deb..066185aa3 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -170,11 +170,9 @@ namespace smt { if (sk_term != 0) { sk_value = sk_term; } - else { - if (m_manager.is_model_value(sk_value)) - return false; - } } + if (m_manager.is_model_value(sk_value)) + return false; bindings.set(num_decls - i - 1, sk_value); } diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index d8f18a123..fea9f9bce 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -102,6 +102,7 @@ namespace smt { return; m_manager.inc_ref(n); m_elems.insert(n, generation); + CTRACE("model_finder", m_manager.is_model_value(n), tout << mk_pp(n, m_manager) << "\n";); SASSERT(!m_manager.is_model_value(n)); }