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

fix #4336 - check return values of eval, they can be null due to cancelation

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-05-16 12:42:51 -07:00
parent a3f56f0d95
commit 843b6cf149
2 changed files with 12 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/bv_decl_plugin.h
View file

@ -412,6 +412,7 @@ public:
app * mk_bv_neg(expr * arg) { return m_manager.mk_app(get_fid(), OP_BNEG, arg); } app * mk_bv_neg(expr * arg) { return m_manager.mk_app(get_fid(), OP_BNEG, arg); }
app * mk_bv_urem(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BUREM, arg1, arg2); } app * mk_bv_urem(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BUREM, arg1, arg2); }
app * mk_bv_srem(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSREM, arg1, arg2); } app * mk_bv_srem(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSREM, arg1, arg2); }
app * mk_bv_smod(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSMOD, arg1, arg2); }
app * mk_bv_add(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BADD, arg1, arg2); } app * mk_bv_add(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BADD, arg1, arg2); }
app * mk_bv_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSUB, arg1, arg2); } app * mk_bv_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSUB, arg1, arg2); }
app * mk_bv_mul(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BMUL, arg1, arg2); } app * mk_bv_mul(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BMUL, arg1, arg2); }

20
src/smt/smt_model_finder.cpp
View file

@ -598,16 +598,16 @@ namespace smt {
for (expr* e : n->get_exceptions()) { for (expr* e : n->get_exceptions()) {
expr * val = eval(e, true); expr * val = eval(e, true);
SASSERT(val != nullptr); if (val)
r.push_back(val); r.push_back(val);
} }
for (node* a : n->get_avoid_set()) { for (node* a : n->get_avoid_set()) {
node * p = a->get_root(); node * p = a->get_root();
if (!p->is_mono_proj() && p->get_else() != nullptr) { if (!p->is_mono_proj() && p->get_else() != nullptr) {
expr * val = eval(p->get_else(), true); expr * val = eval(p->get_else(), true);
SASSERT(val != nullptr); if (val)
r.push_back(val); r.push_back(val);
} }
} }
} }
@ -628,8 +628,9 @@ namespace smt {
for (auto const& kv : elems) { for (auto const& kv : elems) {
expr * t = kv.m_key; expr * t = kv.m_key;
unsigned gen = kv.m_value; unsigned gen = kv.m_value;
expr * t_val = eval(t, true); expr * t_val = eval(t, true);
SASSERT(t_val != nullptr); if (!t_val)
return t_result;
bool found = false; bool found = false;
for (expr* v : ex_vals) { for (expr* v : ex_vals) {
if (!m.are_distinct(t_val, v)) { if (!m.are_distinct(t_val, v)) {
@ -701,7 +702,7 @@ namespace smt {
return false; return false;
for (expr * ex : exceptions) { for (expr * ex : exceptions) {
expr * ex_val = eval(ex, true); expr * ex_val = eval(ex, true);
if (!m.are_distinct(k_interp, ex_val)) { if (ex_val && !m.are_distinct(k_interp, ex_val)) {
SASSERT(m_new_constraints); SASSERT(m_new_constraints);
// This constraint cannot be asserted into m_context during model construction. // This constraint cannot be asserted into m_context during model construction.
// We must save it, and assert it during a restart. // We must save it, and assert it during a restart.
@ -891,7 +892,8 @@ namespace smt {
m_model->register_aux_decl(p, pi); m_model->register_aux_decl(p, pi);
if (n->get_else()) { if (n->get_else()) {
expr * else_val = eval(n->get_else(), true); expr * else_val = eval(n->get_else(), true);
pi->set_else(else_val); if (else_val)
pi->set_else(else_val);
} }
for (expr * v : values) { for (expr * v : values) {
pi->insert_new_entry(&v, v); pi->insert_new_entry(&v, v);
@ -1385,7 +1387,7 @@ namespace smt {
func_decl * get_array_func_decl(app * ground_array, auf_solver & s) { func_decl * get_array_func_decl(app * ground_array, auf_solver & s) {
TRACE("model_evaluator", tout << expr_ref(ground_array, m) << "\n";); TRACE("model_evaluator", tout << expr_ref(ground_array, m) << "\n";);
expr * ground_array_interp = s.eval(ground_array, false); expr * ground_array_interp = s.eval(ground_array, false);
if (ground_array_interp != nullptr && m_array.is_as_array(ground_array_interp)) if (ground_array_interp && m_array.is_as_array(ground_array_interp))
return m_array.get_as_array_func_decl(ground_array_interp); return m_array.get_as_array_func_decl(ground_array_interp);
return nullptr; return nullptr;
} }