From 0270817b31dd089eaba96affcbb79759d2ba74ba Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 16 Jun 2026 11:25:14 -0600
Subject: [PATCH] block lia2card on recursive functions

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/arith/lia2card_tactic.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp
index 17d8de908..c9c675ac0 100644
--- a/src/tactic/arith/lia2card_tactic.cpp
+++ b/src/tactic/arith/lia2card_tactic.cpp
@@ -185,6 +185,10 @@ public:
         expr_safe_replace rep(m);
 
         tactic_report report("lia2card", *g);
+        if (recfun::util(m()).has_rec_defs()) {
+            result.push_back(g.get());
+            return;
+        }
 
         bound_manager bounds(m);
         for (unsigned i = 0; i < g->size(); ++i)