mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-29 08:49:51 +00:00
Code Activity

fix infinite loop in update function

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-11-15 15:47:33 -08:00
parent 11fb5c7dc4
commit 6d19c045d8
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/sls/sls_arith_base.cpp
View file

@ -2707,6 +2707,8 @@ namespace sls {
void arith_base<num_t>::update_unchecked(var_t v, num_t const& new_value) { void arith_base<num_t>::update_unchecked(var_t v, num_t const& new_value) {
auto& vi = m_vars[v]; auto& vi = m_vars[v];
auto old_value = value(v); auto old_value = value(v);
if (old_value == new_value)
return;
IF_VERBOSE(5, verbose_stream() << "update: v" << v << " " << mk_bounded_pp(vi.m_expr, m) << " := " << old_value << " -> " << new_value << "\n"); IF_VERBOSE(5, verbose_stream() << "update: v" << v << " " << mk_bounded_pp(vi.m_expr, m) << " := " << old_value << " -> " << new_value << "\n");
TRACE(arith, tout << "update: v" << v << " " << mk_bounded_pp(vi.m_expr, m) << " := " << old_value << " -> " << new_value << "\n"); TRACE(arith, tout << "update: v" << v << " " << mk_bounded_pp(vi.m_expr, m) << " := " << old_value << " -> " << new_value << "\n");
vi.set_value(new_value); vi.set_value(new_value);