From 295d02397bb9ab1cc3ea7c935b11e122707603a9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Oct 2025 12:48:50 +0200 Subject: [PATCH] Add SASSERT for finite set check in factory Added assertion to check if the sort is a finite set. --- src/model/finite_set_value_factory.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/model/finite_set_value_factory.cpp b/src/model/finite_set_value_factory.cpp index 9ad208d02..10e37c1d1 100644 --- a/src/model/finite_set_value_factory.cpp +++ b/src/model/finite_set_value_factory.cpp @@ -12,7 +12,6 @@ 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), @@ -22,6 +21,7 @@ finite_set_value_factory::finite_set_value_factory(ast_manager & m, family_id fi 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 (m_sort2value_set.find(s, set) && !set->empty()) return *(set->begin());