From 84d592c1f2e42d16842222f1ed60a63661b9bf4c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 16 Feb 2024 09:59:57 +0700 Subject: [PATCH] fix #7121 Signed-off-by: Nikolaj Bjorner --- src/ast/converters/generic_model_converter.cpp | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/ast/converters/generic_model_converter.cpp b/src/ast/converters/generic_model_converter.cpp index 1e81f913149..c50d86cae6d 100644 --- a/src/ast/converters/generic_model_converter.cpp +++ b/src/ast/converters/generic_model_converter.cpp @@ -43,6 +43,7 @@ void generic_model_converter::operator()(model_ref & md) { expr_ref val(m); unsigned arity; bool reset_ev = false; + obj_map> uninterpreted; for (unsigned i = m_entries.size(); i-- > 0; ) { entry const& e = m_entries[i]; switch (e.m_instruction) { @@ -63,6 +64,13 @@ void generic_model_converter::operator()(model_ref & md) { reset_ev = old_val != nullptr; md->register_decl(e.m_f, val); } + // corner case when uninterpreted constants are eliminated + sort* s = e.m_f->get_range(); + if (m.is_uninterp(s) && !md->has_uninterpreted_sort(s)) { + uninterpreted.insert_if_not_there(s, {}); + if (!uninterpreted[s].contains(val)) + uninterpreted[s].push_back(val); + } } else { func_interp * old_val = md->get_func_interp(e.m_f); @@ -84,6 +92,9 @@ void generic_model_converter::operator()(model_ref & md) { break; } } + for (auto const& [s, u] : uninterpreted) { + md->register_usort(s, u.size(), u.data()); + } TRACE("model_converter", tout << "after generic_model_converter\n"; model_v2_pp(tout, *md);); }