mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

use bail_out instead of early return to ensure marks are cleared

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-12-22 06:14:38 +01:00
parent 78ce6c1c6c
commit 65b678dd42
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/pb_solver.cpp
View file

@ -712,7 +712,7 @@ namespace pb {
auto cindex = js.get_ext_justification_idx(); auto cindex = js.get_ext_justification_idx();
auto* ext = sat::constraint_base::to_extension(cindex); auto* ext = sat::constraint_base::to_extension(cindex);
if (ext != this) if (ext != this)
return l_undef; goto bail_out;
constraint& cnstr = index2constraint(cindex); constraint& cnstr = index2constraint(cindex);
++m_stats.m_num_resolves; ++m_stats.m_num_resolves;