diff --git a/src/model/finite_set_value_factory.cpp b/src/model/finite_set_value_factory.cpp
new file mode 100644
index 000000000..df9ef46bc
--- /dev/null
+++ b/src/model/finite_set_value_factory.cpp
@@ -0,0 +1,58 @@
+/*++
+Copyright (c) 2025 Microsoft Corporation
+
+Module Name:
+
+    finite_set_value_factory.cpp
+
+Abstract:
+
+    Factory for creating finite set values
+
+--*/
+#include "model/finite_set_value_factory.h"
+#include "model/model_core.h"
+
+finite_set_value_factory::finite_set_value_factory(ast_manager & m, family_id fid, model_core & md):
+    struct_factory(m, fid, md),
+    u(m) {
+}
+
+expr * finite_set_value_factory::get_some_value(sort * s) {
+    // Check if we already have a value for this sort
+    value_set * set = nullptr;
+    SASSERT(u.is_finite_set(s));
+    #if 0
+    if (m_sort2value_set.find(s, set) && !set->empty()) 
+        return *(set->begin());
+    #endif
+    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
+
+    return nullptr;
+    #if 0
+    value_set * set = get_value_set(s);
+    
+    // If no values have been generated yet, use get_some_value
+    if (set->empty()) {
+        auto r = u.mk_empty(s);
+        register_value(r);
+        return r;
+    }
+    auto e = md.get_fresh_value(elem_sort);
+    if (e) {
+        auto r = u.mk_singleton(e);
+        register_value(r);
+        return r;
+    }
+
+    // For finite domains, we may not be able to generate fresh values
+    // if all values have been exhausted
+    return nullptr;
+    #endif
+}
diff --git a/src/model/finite_set_value_factory.h b/src/model/finite_set_value_factory.h
new file mode 100644
index 000000000..8dbbc7aae
--- /dev/null
+++ b/src/model/finite_set_value_factory.h
@@ -0,0 +1,30 @@
+/*++
+Copyright (c) 2025 Microsoft Corporation
+
+Module Name:
+
+    finite_set_value_factory.h
+
+Abstract:
+
+    Factory for creating finite set values
+
+--*/
+#pragma once
+
+#include "model/struct_factory.h"
+#include "ast/finite_set_decl_plugin.h"
+
+/**
+   \brief Factory for finite set values.
+*/
+class finite_set_value_factory : public struct_factory {
+    finite_set_util u;
+public:
+    finite_set_value_factory(ast_manager & m, family_id fid, model_core & md);
+    
+    expr * get_some_value(sort * s) override;
+    
+    expr * get_fresh_value(sort * s) override;
+};
+