From d9e77ba443aae56a60d0f2d6e7ea33ff032dd7b7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 1 Nov 2018 09:55:27 -0500 Subject: [PATCH] fix model extraction for 0-ary recursive function declarations Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 83ff79d3c..6e132ff71 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4460,6 +4460,11 @@ namespace smt { auto& def = u.get_def(f); expr* rhs = def.get_rhs(); if (!rhs) continue; + if (f->get_arity() == 0) { + m_model->register_decl(f, rhs); + continue; + } + func_interp* fi = alloc(func_interp, m, f->get_arity()); // reverse argument order so that variable 0 starts at the beginning. expr_ref_vector subst(m);