From 1d9c770d74d3072581907c556fc4a8b33e00e3f7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 16 Jun 2026 14:02:24 -0600 Subject: [PATCH] Fix reference to recfun::util in lia2card_tactic.cpp --- src/tactic/arith/lia2card_tactic.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index c9c675ac0..b45457349 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -20,6 +20,7 @@ Notes: #include "ast/ast_ll_pp.h" #include "ast/pb_decl_plugin.h" #include "ast/arith_decl_plugin.h" +#include "ast/recfun_decl_plugin.h" #include "ast/rewriter/rewriter_def.h" #include "ast/rewriter/expr_safe_replace.h" #include "ast/ast_util.h" @@ -185,7 +186,7 @@ public: expr_safe_replace rep(m); tactic_report report("lia2card", *g); - if (recfun::util(m()).has_rec_defs()) { + if (recfun::util(m).has_rec_defs()) { result.push_back(g.get()); return; }