From 48a8269a8dd4c4099d4df4443a344a33ed40fc18 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 16 Oct 2025 12:54:22 +0200
Subject: [PATCH] Refactor finite_set_value_factory for value handling

---
 src/model/finite_set_value_factory.cpp | 43 +++++++++-----------------
 1 file changed, 14 insertions(+), 29 deletions(-)

diff --git a/src/model/finite_set_value_factory.cpp b/src/model/finite_set_value_factory.cpp
index 10e37c1d1..c0937314c 100644
--- a/src/model/finite_set_value_factory.cpp
+++ b/src/model/finite_set_value_factory.cpp
@@ -15,7 +15,7 @@ Abstract:
 
 finite_set_value_factory::finite_set_value_factory(ast_manager & m, family_id fid, model_core & md):
     struct_factory(m, fid, md),
-    m_util(m) {
+    u(m) {
 }
 
 expr * finite_set_value_factory::get_some_value(sort * s) {
@@ -24,41 +24,26 @@ expr * finite_set_value_factory::get_some_value(sort * s) {
     SASSERT(u.is_finite_set(s));
     if (m_sort2value_set.find(s, set) && !set->empty()) 
         return *(set->begin());
-
-    // For sets, return an empty set
-    if (m_util.is_array(s)) {
-        expr * empty = m_util.mk_empty_set(s);
-        register_value(empty);
-        return empty;
-    }
-
-    return nullptr;
+    return u.mk_empty(s);
 }
 
 expr * finite_set_value_factory::get_fresh_value(sort * s) {
+    sort* elem_sort = nullptr;
+    VERIFY(u.is_finite_set(s, elem_sort));
     // Get a fresh value for a finite set sort
     value_set * set = get_value_set(s);
     
     // If no values have been generated yet, use get_some_value
-    if (set->empty()) 
-        return get_some_value(s);
-
-    // For sets represented as arrays
-    if (m_util.is_array(s)) {
-        // Get the element sort (domain of the array)
-        sort * elem_sort = get_array_domain(s, 0);
-        
-        // Try to get a fresh value from the element domain
-        expr * fresh_elem = m_model.get_fresh_value(elem_sort);
-        if (fresh_elem != nullptr) {
-            // Create a singleton set with the fresh element
-            // Start with an empty set and add the element
-            expr * empty = m_util.mk_empty_set(s);
-            expr * args[3] = { empty, fresh_elem, m_manager.mk_true() };
-            expr * singleton = m_util.mk_store(3, args);
-            register_value(singleton);
-            return singleton;
-        }
+    if (set->empty()) {
+        auto r = u.mk_empty(s);
+        set->insert(r);
+        return r;
+    }
+    auto e = md.get_fresh_value(elem_sort);
+    if (e) {
+        auto r = u.mk_singleton(e);
+        set->insert(r);
+        return r;
     }
 
     // For finite domains, we may not be able to generate fresh values