diff --git a/src/model/finite_set_value_factory.cpp b/src/model/finite_set_value_factory.cpp
index 2b3ed95cc..9ad208d02 100644
--- a/src/model/finite_set_value_factory.cpp
+++ b/src/model/finite_set_value_factory.cpp
@@ -12,9 +12,11 @@ Abstract:
 --*/
 #include "model/finite_set_value_factory.h"
 #include "model/model_core.h"
+#include "ast/array_decl_plugin.h"
 
 finite_set_value_factory::finite_set_value_factory(ast_manager & m, family_id fid, model_core & md):
-    struct_factory(m, fid, md) {
+    struct_factory(m, fid, md),
+    m_util(m) {
 }
 
 expr * finite_set_value_factory::get_some_value(sort * s) {
@@ -23,7 +25,12 @@ expr * finite_set_value_factory::get_some_value(sort * s) {
     if (m_sort2value_set.find(s, set) && !set->empty()) 
         return *(set->begin());
 
-    // TODO add handling here
+    // 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;
 }
@@ -36,9 +43,23 @@ expr * finite_set_value_factory::get_fresh_value(sort * s) {
     if (set->empty()) 
         return get_some_value(s);
 
-    // TODO add handling here: create a fresh value for the element sort.
-    // if it fails, then traverse set to add a new value to a set such that
-    // the new set hasn't been created before.
+    // 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;
+        }
+    }
 
     // For finite domains, we may not be able to generate fresh values
     // if all values have been exhausted
diff --git a/src/model/finite_set_value_factory.h b/src/model/finite_set_value_factory.h
index 51afd03e6..68e19796a 100644
--- a/src/model/finite_set_value_factory.h
+++ b/src/model/finite_set_value_factory.h
@@ -13,11 +13,13 @@ Abstract:
 #pragma once
 
 #include "model/struct_factory.h"
+#include "ast/array_decl_plugin.h"
 
 /**
    \brief Factory for finite set values.
 */
 class finite_set_value_factory : public struct_factory {
+    array_util m_util;
 public:
     finite_set_value_factory(ast_manager & m, family_id fid, model_core & md);