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)