From 49779a2492fcebdc247dc8a3baa39427f3825fd6 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Tue, 14 Oct 2025 17:10:38 +0000
Subject: [PATCH] Fix order of checks in mk_in to handle singleton same element
 case first

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/ast/rewriter/finite_set_rewriter.cpp | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/ast/rewriter/finite_set_rewriter.cpp b/src/ast/rewriter/finite_set_rewriter.cpp
index 1e5e5fa0a..3773a6483 100644
--- a/src/ast/rewriter/finite_set_rewriter.cpp
+++ b/src/ast/rewriter/finite_set_rewriter.cpp
@@ -176,23 +176,23 @@ br_status finite_set_rewriter::mk_singleton(expr * arg, expr_ref & result) {
 }
 
 br_status finite_set_rewriter::mk_in(expr * elem, expr * set, expr_ref & result) {
-    // set.in(x, singleton(y)) -> x = y
-    expr* singleton_elem;
-    if (m_util.is_singleton(set, singleton_elem)) {
-        result = m().mk_eq(elem, singleton_elem);
-        return BR_REWRITE1;
-    }
-    
     // set.in(x, empty) -> false
     if (m_util.is_empty(set)) {
         result = m().mk_false();
         return BR_DONE;
     }
     
-    // set.in(x, singleton(x)) -> true (when x is the same)
-    if (m_util.is_singleton(set, singleton_elem) && elem == singleton_elem) {
-        result = m().mk_true();
-        return BR_DONE;
+    // set.in(x, singleton(y)) checks
+    expr* singleton_elem;
+    if (m_util.is_singleton(set, singleton_elem)) {
+        // set.in(x, singleton(x)) -> true (when x is the same)
+        if (elem == singleton_elem) {
+            result = m().mk_true();
+            return BR_DONE;
+        }
+        // set.in(x, singleton(y)) -> x = y (when x != y)
+        result = m().mk_eq(elem, singleton_elem);
+        return BR_REWRITE1;
     }
     
     return BR_FAILED;