mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-10 07:10:30 +00:00
Code Activity

Fix null pointer dereferences and uninitialized variables from discussion #8891

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-09 16:51:12 +00:00
parent 9dcd01c52b
commit 391febed3b
5 changed files with 14 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/euf/euf_mam.cpp
View file

@ -1402,6 +1402,7 @@ namespace euf {
// to check it again.
get_check_mark(reg) == NOT_CHECKED &&
is_ground(m_registers[reg]) &&
instr->m_enode != nullptr &&
get_pat_lbl_hash(reg) == instr->m_enode->get_lbl_hash();
}

8
src/ast/sls/sls_euf_plugin.cpp
View file

@ -289,23 +289,23 @@ namespace sls {
b = g.find(to_app(e)->get_arg(1));
}
if (lit.sign() && m.is_eq(e)) {
if (a->get_root() == b->get_root()) {
if (a && b && a->get_root() == b->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not disequal " << lit << " " << mk_pp(e, m) << "\n");
ctx.display(verbose_stream());
UNREACHABLE();
}
}
else if (!lit.sign() && m.is_eq(e)) {
if (a->get_root() != b->get_root()) {
if (a && b && a->get_root() != b->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not equal " << lit << " " << mk_pp(e, m) << "\n");
//UNREACHABLE();
}
}
else if (to_app(e)->get_family_id() != basic_family_id && lit.sign() && g.find(e)->get_root() != g.find(m.mk_false())->get_root()) {
else if (to_app(e)->get_family_id() != basic_family_id && lit.sign() && g.find(e) && g.find(m.mk_false()) && g.find(e)->get_root() != g.find(m.mk_false())->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not alse " << lit << " " << mk_pp(e, m) << "\n");
//UNREACHABLE();
}
else if (to_app(e)->get_family_id() != basic_family_id && !lit.sign() && g.find(e)->get_root() != g.find(m.mk_true())->get_root()) {
else if (to_app(e)->get_family_id() != basic_family_id && !lit.sign() && g.find(e) && g.find(m.mk_true()) && g.find(e)->get_root() != g.find(m.mk_true())->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not true " << lit << " " << mk_pp(e, m) << "\n");
//UNREACHABLE();
}

6
src/math/realclosure/realclosure.cpp
View file

@ -3458,6 +3458,8 @@ namespace realclosure {
if (sc) sc = sc->prev();
i--;
}
if (!sc)
return 0;
return ext->sdt()->qs()[sc->qidx()].size();
}
@ -3474,6 +3476,8 @@ namespace realclosure {
if (sc) sc = sc->prev();
i--;
}
if (!sc)
return 0;
const polynomial & q = ext->sdt()->qs()[sc->qidx()];
return q.size();
}
@ -3491,6 +3495,8 @@ namespace realclosure {
if (sc) sc = sc->prev();
i--;
}
if (!sc)
return numeral();
const polynomial & q = ext->sdt()->qs()[sc->qidx()];
if (j >= q.size())
return numeral();

4
src/muz/spacer/spacer_context.cpp
View file

@ -3330,7 +3330,7 @@ bool context::is_reachable(pob &n)
model_ref mdl;
// used in case n is reachable
bool is_concrete;
bool is_concrete = false;
const datalog::rule * r = nullptr;
// denotes which predecessor's (along r) reach facts are used
bool_vector reach_pred_used;
@ -3521,7 +3521,7 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
model_ref model;
// used in case n is reachable
bool is_concrete;
bool is_concrete = false;
const datalog::rule * r = nullptr;
// denotes which predecessor's (along r) reach facts are used
bool_vector reach_pred_used;

1
src/smt/mam.cpp
View file

@ -1360,6 +1360,7 @@ namespace {
// to check it again.
get_check_mark(reg) == NOT_CHECKED &&
is_ground(m_registers[reg]) &&
instr->m_enode != nullptr &&
get_pat_lbl_hash(reg) == instr->m_enode->get_lbl_hash();
}