mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
handle constants
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
09696e989e
commit
8f306c6a8f
|
@ -133,8 +133,12 @@ void model_core::add_lambda_defs() {
|
|||
quantifier* q = m.is_lambda_def(f);
|
||||
if (!q)
|
||||
continue;
|
||||
func_interp* fi = alloc(func_interp, m, f->get_arity());
|
||||
fi->set_else(q);
|
||||
register_decl(f, fi);
|
||||
if (f->get_arity() > 0) {
|
||||
func_interp* fi = alloc(func_interp, m, f->get_arity());
|
||||
fi->set_else(q);
|
||||
register_decl(f, fi);
|
||||
}
|
||||
else
|
||||
register_decl(f, q);
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue