From 2bff0a6b8a4697d8450d38b5362d6c33352d9d11 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 6 Jun 2023 16:35:37 -0700 Subject: [PATCH] regression on quantifier weight computation when weights are 0 vs non-0. It modifies a change made for the fix of #2667. That fix caused a regression in F*. Reported @mtzguido Signed-off-by: Nikolaj Bjorner --- src/smt/qi_queue.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index 582bcc664..781ed7c49 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -131,6 +131,8 @@ namespace smt { // max_top_generation and min_top_generation are not available for computing inc_gen set_values(q, nullptr, generation, 0, 0, cost); float r = m_evaluator(m_new_gen_function, m_vals.size(), m_vals.data()); + if (q->get_weight() > 0 || r > 0) + return static_cast(r); return std::max(generation + 1, static_cast(r)); }