From 0218a15f2eb70fc68328d9dc913e83a3523668a3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 16 Oct 2024 20:59:28 -0700 Subject: [PATCH] fixup finite domain search Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_datatype_plugin.cpp | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/ast/sls/sls_datatype_plugin.cpp b/src/ast/sls/sls_datatype_plugin.cpp index 981ddb798..8a6c1c64b 100644 --- a/src/ast/sls/sls_datatype_plugin.cpp +++ b/src/ast/sls/sls_datatype_plugin.cpp @@ -323,21 +323,23 @@ namespace sls { continue; auto con = get_constructor(n); if (!con) { - m_values.setx(id, m_model->get_fresh_value(e->get_sort())); + auto v = m_model->get_fresh_value(e->get_sort()); + if (!v) + v = m_model->get_some_value(e->get_sort()); + SASSERT(v); + m_values.setx(id, v); TRACE("dt", tout << "Fresh interpretation " << g->bpp(n) << " <- " << mk_bounded_pp(m_values.get(id), m) << "\n"); continue; } auto f = con->get_decl(); args.reset(); for (auto arg : euf::enode_args(con)) { - if (dt.is_datatype(arg->get_sort())) { - auto val_arg = m_values.get(arg->get_root_id()); - SASSERT(val_arg); - args.push_back(val_arg); - } + if (dt.is_datatype(arg->get_sort())) + args.push_back(m_values.get(arg->get_root_id())); else args.push_back(ctx.get_value(arg->get_expr())); } + SASSERT(all_of(args, [&](expr* e) { return e != nullptr; })); m_values.setx(id, m.mk_app(f, args)); TRACE("dt", tout << "Patched interpretation " << g->bpp(n) << " <- " << mk_bounded_pp(m_values.get(id), m) << "\n"); }