diff --git a/src/model/finite_set_value_factory.cpp b/src/model/finite_set_value_factory.cpp
index 04f574c50..9fee35d9e 100644
--- a/src/model/finite_set_value_factory.cpp
+++ b/src/model/finite_set_value_factory.cpp
@@ -63,7 +63,7 @@ expr * finite_set_value_factory::get_fresh_value(sort * s) {
         N *= 2;
     }
     
-    auto r = u.mk_union(values.get(values.size() - N), values.back());
+    auto r = u.mk_union(values.get(values.size() - N), values.get(N));
     register_value(r);
     return r;
 }
\ No newline at end of file