From 9d09a050e8d5d0fb179e1b736b85cc0a7c434c8b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 27 May 2026 14:37:37 -0700
Subject: [PATCH] use max-top-generation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_quantifier.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 4db888a2e..ac18bd5e0 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -489,7 +489,7 @@ namespace smt {
                                           unsigned min_top_generation,
                                           unsigned max_top_generation,
                                           vector<std::tuple<enode *, enode *>> & used_enodes) {
-        return m_imp->add_instance(q, pat, num_bindings, bindings, def, max_generation, min_top_generation, max_generation, used_enodes);
+        return m_imp->add_instance(q, pat, num_bindings, bindings, def, max_generation, min_top_generation, max_top_generation, used_enodes);
     }
 
     bool quantifier_manager::add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, expr* def, unsigned generation) {