From 3d910028bf4ecdd3386d73816d186588a8065a00 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 27 Sep 2013 16:55:05 +0100 Subject: [PATCH] fixed potential performance problem with fully interpreted sorts in the quantifier instantiation. Signed-off-by: Christoph M. Wintersteiger --- src/smt/smt_model_finder.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index c4a48d9f8..8303d05ac 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -975,9 +975,11 @@ namespace smt { // Moreover, a model assigns an arbitrary intepretation to these sorts using "model_values" a model value. // If these module values "leak" inside the logical context, they may affect satisfiability. // - // n->insert(m_model->get_some_value(n->get_sort()), 0); - // TODO: we can use get_some_value if the sort n->get_sort() does not depend on any uninterpreted sorts. - n->insert(m_manager.mk_fresh_const("elem", n->get_sort()), 0); + sort * ns = n->get_sort(); + if (m_manager.is_fully_interp(ns)) + n->insert(m_model->get_some_value(ns), 0); + else + n->insert(m_manager.mk_fresh_const("elem", ns), 0); } } }