From c1665a5cad20b884b0bc08aecc54b7d89ac883b9 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 15 Oct 2025 19:41:05 +0000
Subject: [PATCH] Refine is_fully_interp implementation with SASSERT

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/ast/finite_set_decl_plugin.cpp | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp
index 5cd1fd035..4d669e12a 100644
--- a/src/ast/finite_set_decl_plugin.cpp
+++ b/src/ast/finite_set_decl_plugin.cpp
@@ -183,12 +183,9 @@ expr * finite_set_decl_plugin::get_some_value(sort * s) {
 }
 
 bool finite_set_decl_plugin::is_fully_interp(sort * s) const {
-    if (!is_finite_set(s))
-        return false;
+    SASSERT(is_finite_set(s));
     sort* element_sort = get_element_sort(s);
-    if (!element_sort)
-        return false;
-    return m_manager->is_fully_interp(element_sort);
+    return element_sort && m_manager->is_fully_interp(element_sort);
 }
 
 bool finite_set_decl_plugin::is_value(app * e) const {