From d61df6b91f1679a17978eb04a0e085422448f84c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 30 Aug 2017 20:35:31 +0100 Subject: [PATCH] Model completion bug fix --- src/cmd_context/cmd_context.cpp | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index acbdc0bcf..aa2bb0554 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1701,9 +1701,14 @@ void cmd_context::complete_model() { func_decl * f = v.get_entry(i); if (!md->has_interpretation(f)) { sort * range = f->get_range(); - func_interp * fi = alloc(func_interp, m(), f->get_arity()); - fi->set_else(m().get_some_value(range)); - md->register_decl(f, fi); + expr * some_val = m().get_some_value(range); + if (f->get_arity() > 0) { + func_interp * fi = alloc(func_interp, m(), f->get_arity()); + fi->set_else(some_val); + md->register_decl(f, fi); + } + else + md->register_decl(f, some_val); } } }