mirror of
https://github.com/Z3Prover/z3
synced 2025-06-06 06:03:23 +00:00
avoid deref on null
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
69783db5e8
commit
41c68d64d4
2 changed files with 4 additions and 7 deletions
|
@ -4027,8 +4027,3 @@ namespace smt {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
#ifdef Z3DEBUG
|
|
||||||
void pp(code_tree * c) {
|
|
||||||
c->display(std::cout);
|
|
||||||
}
|
|
||||||
#endif
|
|
||||||
|
|
|
@ -3370,8 +3370,10 @@ namespace smt {
|
||||||
if (u.get_rec_funs().empty()) {
|
if (u.get_rec_funs().empty()) {
|
||||||
model_ref mdl;
|
model_ref mdl;
|
||||||
get_model(mdl);
|
get_model(mdl);
|
||||||
for (theory* t : m_theory_set) {
|
if (mdl.get()) {
|
||||||
t->validate_model(*mdl);
|
for (theory* t : m_theory_set) {
|
||||||
|
t->validate_model(*mdl);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
#if 0
|
#if 0
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue