mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
create empty model
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
dd6e76478d
commit
1fc1249bef
|
@ -176,10 +176,10 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, p
|
|||
if (mc.get()) {
|
||||
(*mc)(labels);
|
||||
model_converter2model(m, mc.get(), md);
|
||||
if (!md) {
|
||||
// create empty model.
|
||||
md = alloc(model, m);
|
||||
}
|
||||
}
|
||||
if (!md) {
|
||||
// create empty model.
|
||||
md = alloc(model, m);
|
||||
}
|
||||
return l_true;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue