From 8f306c6a8fec4b80e89d19cbec391f06d915ed6b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 Aug 2021 11:59:41 -0700 Subject: [PATCH] handle constants Signed-off-by: Nikolaj Bjorner --- src/model/model_core.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index 1ed6e3670..81ec4c654 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -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); } }