mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 04:03:39 +00:00
fix debug build
This commit is contained in:
parent
ecc302bdc8
commit
60fb53ad34
|
@ -251,7 +251,7 @@ namespace sls {
|
||||||
template<typename num_t>
|
template<typename num_t>
|
||||||
double arith_lookahead<num_t>::lookahead(expr* t, bool update_score) {
|
double arith_lookahead<num_t>::lookahead(expr* t, bool update_score) {
|
||||||
ctx.rlimit().inc();
|
ctx.rlimit().inc();
|
||||||
SASSERT(a.is_int_real(t) || m.is_bool(t));
|
SASSERT(autil.is_int_real(t) || m.is_bool(t));
|
||||||
double score = m_top_score;
|
double score = m_top_score;
|
||||||
for (unsigned depth = m_min_depth; depth <= m_max_depth; ++depth) {
|
for (unsigned depth = m_min_depth; depth <= m_max_depth; ++depth) {
|
||||||
for (unsigned i = 0; i < m_update_stack[depth].size(); ++i) {
|
for (unsigned i = 0; i < m_update_stack[depth].size(); ++i) {
|
||||||
|
|
Loading…
Reference in a new issue