diff --git a/src/ast/sls/sls_bv_eval.cpp b/src/ast/sls/sls_bv_eval.cpp index 5522076a0..c4f2dbb64 100644 --- a/src/ast/sls/sls_bv_eval.cpp +++ b/src/ast/sls/sls_bv_eval.cpp @@ -679,7 +679,7 @@ namespace sls { ++m_lookahead_steps; if (m_lookahead_steps < m_lookahead_phase_size) return true; - if (m_lookahead_steps > 2 * m_lookahead_phase_size) + if (m_lookahead_steps > 10 * m_lookahead_phase_size) m_lookahead_steps = 0; return false; } diff --git a/src/ast/sls/sls_bv_eval.h b/src/ast/sls/sls_bv_eval.h index b6ac73e63..3f5f87024 100644 --- a/src/ast/sls/sls_bv_eval.h +++ b/src/ast/sls/sls_bv_eval.h @@ -53,7 +53,7 @@ namespace sls { config m_config; bool_vector m_fixed; unsigned m_lookahead_steps = 0; - unsigned m_lookahead_phase_size = 100; + unsigned m_lookahead_phase_size = 10; scoped_ptr_vector m_values; // expr-id -> bv valuation