mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
revert debug only changes to sat-solver
This commit is contained in:
parent
c5e33b79b5
commit
daeaed1e82
|
@ -2974,7 +2974,7 @@ namespace sat {
|
||||||
}
|
}
|
||||||
|
|
||||||
bool solver::should_rephase() {
|
bool solver::should_rephase() {
|
||||||
return m_conflicts_since_init > 5 && m_conflicts_since_init > m_rephase_lim;
|
return m_conflicts_since_init > m_rephase_lim;
|
||||||
}
|
}
|
||||||
|
|
||||||
void solver::do_rephase() {
|
void solver::do_rephase() {
|
||||||
|
@ -3023,7 +3023,7 @@ namespace sat {
|
||||||
UNREACHABLE();
|
UNREACHABLE();
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
m_rephase_inc = m_config.m_rephase_base;
|
m_rephase_inc += m_config.m_rephase_base;
|
||||||
m_rephase_lim += m_rephase_inc;
|
m_rephase_lim += m_rephase_inc;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue