From 6fef24edb4b708957c91447bd9644c4cc1a84939 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 3 Mar 2016 08:07:06 -0800
Subject: [PATCH] recursive function definitions; combine model-building
 functionality

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_model_checker.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index c1befd545..e4bfcc806 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -329,10 +329,11 @@ namespace smt {
                 sub(q->get_expr(), num_decls, args.c_ptr(), tmp);
                 m_curr_model->eval(tmp, result, true);
                 if (m.is_false(result)) {
-                    TRACE("model_checker", tout << tmp << "\nevaluates to:\n" << result << "\n";);                    
                     add_instance(q, args, 0);
                     return false;
                 }
+                TRACE("model_checker", tout << tmp << "\nevaluates to:\n" << result << "\n";);
+                // if (!m.is_true(result)) is_undef = true;
             }
         }
         return !is_undef;