mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
remove on-the fly ackerman reduction because it interferes with conflict resolution
This commit is contained in:
parent
b758d5b2b1
commit
3bf1b606df
|
@ -74,14 +74,7 @@ namespace euf {
|
|||
m.inc_ref(inf->c);
|
||||
new_tmp();
|
||||
}
|
||||
other->m_count++;
|
||||
if (other->m_count > m_high_watermark) {
|
||||
if (other->is_cc)
|
||||
add_cc(other->a, other->b);
|
||||
else
|
||||
add_eq(other->a, other->b, other->c);
|
||||
other->m_count = 0;
|
||||
}
|
||||
other->m_count++;
|
||||
inference::push_to_front(m_queue, other);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue