From d3e262af85f44a5cae94562c2deb0aaf62af3b76 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 16 Oct 2025 12:56:05 +0200
Subject: [PATCH] Use register_value instead of direct set insertion

Replaced direct insertion into set with register_value calls.
---
 src/model/finite_set_value_factory.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/model/finite_set_value_factory.cpp b/src/model/finite_set_value_factory.cpp
index c0937314c..39c361a0f 100644
--- a/src/model/finite_set_value_factory.cpp
+++ b/src/model/finite_set_value_factory.cpp
@@ -36,13 +36,13 @@ expr * finite_set_value_factory::get_fresh_value(sort * s) {
     // If no values have been generated yet, use get_some_value
     if (set->empty()) {
         auto r = u.mk_empty(s);
-        set->insert(r);
+        register_value(r);
         return r;
     }
     auto e = md.get_fresh_value(elem_sort);
     if (e) {
         auto r = u.mk_singleton(e);
-        set->insert(r);
+        register_value(r);
         return r;
     }