From 26d37c7b308aaec026579df9be7b8e839e2fb9dd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Oct 2025 13:29:38 +0200 Subject: [PATCH] fixup Signed-off-by: Nikolaj Bjorner --- src/model/finite_set_value_factory.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/model/finite_set_value_factory.cpp b/src/model/finite_set_value_factory.cpp index 135ad60df..981075954 100644 --- a/src/model/finite_set_value_factory.cpp +++ b/src/model/finite_set_value_factory.cpp @@ -40,9 +40,10 @@ expr * finite_set_value_factory::get_fresh_value(sort * s) { register_value(r); return r; } - auto e = md.get_fresh_value(elem_sort); + auto e = m_model.get_fresh_value(elem_sort); if (e) { auto r = u.mk_singleton(e); + register_value(e); // register e so we can access the finite domain within this class register_value(r); return r; }