From e5d731967055e9e3a30e3ce576d68954a6fc787d Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 21 Feb 2026 02:08:04 +0000
Subject: [PATCH] Code simplifications for finite set plugin

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

diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp
index 49ee4e2bf..6991173b0 100644
--- a/src/ast/finite_set_decl_plugin.cpp
+++ b/src/ast/finite_set_decl_plugin.cpp
@@ -16,7 +16,7 @@ Author:
 Revision History:
 
 --*/
-#include<sstream>
+#include <sstream>
 #include "ast/finite_set_decl_plugin.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/array_decl_plugin.h"
@@ -24,8 +24,7 @@ Revision History:
 #include "ast/ast_pp.h"
 #include "util/warning.h"
 
-finite_set_decl_plugin::finite_set_decl_plugin():
-    m_init(false) {
+finite_set_decl_plugin::finite_set_decl_plugin() {
     m_names.resize(LAST_FINITE_SET_OP, nullptr);
     m_names[OP_FINITE_SET_EMPTY] = "set.empty";
     m_names[OP_FINITE_SET_SINGLETON] = "set.singleton";
@@ -279,11 +278,11 @@ bool finite_set_decl_plugin::is_value(app * e) const {
             continue;
         }
         
+        // Check if it's a union, intersection, or difference
         bool is_setop = 
             is_app_of(a, m_family_id, OP_FINITE_SET_UNION) 
             || is_app_of(a, m_family_id, OP_FINITE_SET_INTERSECT)
             || is_app_of(a, m_family_id, OP_FINITE_SET_DIFFERENCE);
-        // Check if it's a union
         if (is_setop) {
             // Add arguments to todo list
             for (auto arg : *a) 
@@ -297,8 +296,6 @@ bool finite_set_decl_plugin::is_value(app * e) const {
                     return false;
             continue;
         }
-
-        // can add also ranges where lo and hi are values.
         
         // If it's none of the above, it's not a value
         return false;
diff --git a/src/ast/finite_set_decl_plugin.h b/src/ast/finite_set_decl_plugin.h
index ec927dfa9..ea9ab19f0 100644
--- a/src/ast/finite_set_decl_plugin.h
+++ b/src/ast/finite_set_decl_plugin.h
@@ -56,7 +56,7 @@ enum finite_set_op_kind {
 class finite_set_decl_plugin : public decl_plugin {
     ptr_vector<polymorphism::psig>   m_sigs;
     svector<char const*>             m_names;
-    bool                             m_init = false;
+    bool                             m_init{false};
 
     void init();
     func_decl * mk_empty(sort* set_sort);