From 81678923a10df91f1513d8ca440dfdc79c29b818 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 30 Dec 2024 11:09:35 -0800 Subject: [PATCH] take into account for empty vars Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_bv_lookahead.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp index 8db2c9ffa..57fa61370 100644 --- a/src/ast/sls/sls_bv_lookahead.cpp +++ b/src/ast/sls/sls_bv_lookahead.cpp @@ -99,6 +99,8 @@ namespace sls { * random update: select a variable at random and set bits to random values */ bool bv_lookahead::apply_random_update(ptr_vector const& vars) { + if (vars.empty()) + return false; expr* e = vars[ctx.rand(vars.size())]; auto& v = wval(e); m_v_updated.set_bw(v.bw); @@ -136,7 +138,6 @@ namespace sls { * those with high score, but back off if they are frequently chosen. */ ptr_vector const& bv_lookahead::get_candidate_uninterp() { - auto const& lits = ctx.root_literals(); app* e = nullptr; if (m_config.ucb) { double max = -1.0; @@ -166,10 +167,11 @@ namespace sls { return m_empty_vars; auto const& vars = m_ev.terms.uninterp_occurs(e); - VERIFY(!vars.empty()); + TRACE("bv", tout << "candidates " << mk_bounded_pp(e, m) << ": "; for (auto e : vars) tout << mk_bounded_pp(e, m) << " "; tout << "\n";); + //VERIFY(!vars.empty()); return vars; }