mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-27 02:48:48 +00:00
Code Activity

block lia2card on recursive functions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-16 11:25:14 -06:00
parent 66795ea322
commit 0270817b31
1 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/tactic/arith/lia2card_tactic.cpp
View file

@ -185,6 +185,10 @@ public:
expr_safe_replace rep(m); expr_safe_replace rep(m);
tactic_report report("lia2card", *g); tactic_report report("lia2card", *g);
if (recfun::util(m()).has_rec_defs()) {
result.push_back(g.get());
return;
}
bound_manager bounds(m); bound_manager bounds(m);
for (unsigned i = 0; i < g->size(); ++i) for (unsigned i = 0; i < g->size(); ++i)