From ec12368b548a91c21dc6f80e00ccea7d2322aae7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 2 Nov 2015 11:36:50 -0800 Subject: [PATCH] Enable model construction and evaluation for theory functions that may be uninterpreted. To fix issue #237 Signed-off-by: Nikolaj Bjorner --- src/model/model_evaluator.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 79b9209ab..67704719b 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -154,7 +154,7 @@ struct evaluator_cfg : public default_rewriter_cfg { st = m_f_rw.mk_app_core(f, num, args, result); // allow for model evaluation to work on result of rewriting. - if (st == BR_DONE) { + if (st == BR_DONE && is_app(result) && to_app(result)->get_num_args() > 0) { return BR_REWRITE1; }