mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

check for null before debug assertions

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-12-30 09:44:23 -08:00
parent d8741b4aec
commit 4773bec975
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/ast/sls/sls_bv_lookahead.cpp
View file

@ -465,11 +465,12 @@ namespace sls {
*/ */
bool bv_lookahead::apply_update(expr* e, bvect const& new_value, char const* reason) { bool bv_lookahead::apply_update(expr* e, bvect const& new_value, char const* reason) {
if (!e || !wval(e).can_set(new_value))
return false;
SASSERT(bv.is_bv(e)); SASSERT(bv.is_bv(e));
SASSERT(is_uninterp(e)); SASSERT(is_uninterp(e));
SASSERT(m_restore.empty()); SASSERT(m_restore.empty());
if (!e || !wval(e).can_set(new_value))
return false;
wval(e).eval = new_value; wval(e).eval = new_value;
double old_top_score = m_top_score; double old_top_score = m_top_score;