mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

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

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-06-06 16:35:37 -07:00
parent 68f43ac7a4
commit 2bff0a6b8a
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/qi_queue.cpp
View file

@ -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<unsigned>(r);
return std::max(generation + 1, static_cast<unsigned>(r));
}