From 2b5b9854925b0fe1466c7ee4ac80f49b497a7778 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 20 Sep 2025 02:18:44 -0700
Subject: [PATCH] fix divergence regression

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/opt_context.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 2d2a2b494..6244533f0 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -1055,6 +1055,8 @@ namespace opt {
                 continue;            
             return false;
         }
+        if (min_cardinality == UINT_MAX)
+            return false;
         expr_ref_vector new_fmls(m);
         expr_ref_vector soft(m);
         for (unsigned k = 1; k <= min_cardinality; ++k) {