From 9fcede12850c2f3ac457ac90acaa3501e972122f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 23 Nov 2025 09:09:55 -0800
Subject: [PATCH] check cancelation in invariant checker

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/sls/sls_arith_base.cpp | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
index df40b0251..eeb866ba3 100644
--- a/src/ast/sls/sls_arith_base.cpp
+++ b/src/ast/sls/sls_arith_base.cpp
@@ -2588,6 +2588,8 @@ namespace sls {
 
     template<typename num_t>
     void arith_base<num_t>::invariant() {
+        if (m.limit().is_canceled())
+            return;
         for (unsigned v = 0; v < ctx.num_bool_vars(); ++v) {
             auto ineq = get_ineq(v);
             if (ineq)
@@ -2620,10 +2622,10 @@ namespace sls {
                 display(out, ad) << "\n";
             }
         };
-        for (var_t v = 0; v < m_vars.size(); ++v) {            
+        for (var_t v = 0; v < m_vars.size(); ++v) {
             if (!eval_is_correct(v)) {
-//                if (m.rlimit().is_canceled())
-//                    return;
+                if (m.limit().is_canceled())
+                    return;
                 report_error(verbose_stream(), v);
                 TRACE(arith, report_error(tout, v));
                 UNREACHABLE();