diff --git a/src/model/finite_set_value_factory.cpp b/src/model/finite_set_value_factory.cpp
index 39c361a0f..df9ef46bc 100644
--- a/src/model/finite_set_value_factory.cpp
+++ b/src/model/finite_set_value_factory.cpp
@@ -22,8 +22,10 @@ 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);
 }
 
@@ -31,6 +33,9 @@ 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
@@ -49,4 +54,5 @@ expr * finite_set_value_factory::get_fresh_value(sort * s) {
     // For finite domains, we may not be able to generate fresh values
     // if all values have been exhausted
     return nullptr;
+    #endif
 }