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

fix #3055, bound iterations of subpaving

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-21 20:36:58 -08:00
parent 589db2052a
commit ab9bcfdcce
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/math/subpaving/subpaving_t_def.h
View file

@ -1747,9 +1747,8 @@ void context_t<C>::propagate(node * n, bound * b) {
template<typename C> template<typename C>
void context_t<C>::propagate(node * n) { void context_t<C>::propagate(node * n) {
while (m_qhead < m_queue.size()) { unsigned num_nodes = num_vars();
if (inconsistent(n)) while (!inconsistent(n) && m_qhead < m_queue.size() && 2*m_qhead < num_nodes) {
break;
checkpoint(); checkpoint();
bound * b = m_queue[m_qhead]; bound * b = m_queue[m_qhead];
SASSERT(is_bound_of(b, n)); SASSERT(is_bound_of(b, n));