handle constants

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Aug 27, 2021 · 8f306c6 · 8f306c6
1 parent 09696e9
commit 8f306c6
Showing 1 changed file with 7 additions and 3 deletions.
diff --git 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);
     }
 }