mirror of
https://github.com/Z3Prover/z3
synced 2025-05-11 09:44:43 +00:00
fix #4447, or mask it
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
af90992858
commit
743573aac5
3 changed files with 14 additions and 21 deletions
|
@ -4483,9 +4483,9 @@ namespace smt {
|
|||
return false;
|
||||
}
|
||||
|
||||
void context::get_model(model_ref & m) {
|
||||
if (inconsistent())
|
||||
m = nullptr;
|
||||
void context::get_model(model_ref & mdl) {
|
||||
if (inconsistent() || !m.inc())
|
||||
mdl = nullptr;
|
||||
else {
|
||||
mk_proto_model();
|
||||
if (!m_model && m_proto_model) {
|
||||
|
@ -4497,7 +4497,7 @@ namespace smt {
|
|||
// no op
|
||||
}
|
||||
}
|
||||
m = m_model.get();
|
||||
mdl = m_model.get();
|
||||
}
|
||||
}
|
||||
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue