From b97d694e5e2af7e425ad674866a4d697940904f6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 5 Apr 2016 22:26:57 +0200
Subject: [PATCH] undo model evaluation to BR_FULL pending regression in
 assertion violation

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

diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 3eba22267..3111f2b6c 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -118,7 +118,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
             expr * val = m_model.get_const_interp(f);
             if (val != 0) {
                 result = val;
-                return m().is_value(val)?BR_DONE:BR_REWRITE_FULL;
+                return BR_DONE;
+//                return m().is_value(val)?BR_DONE:BR_REWRITE_FULL;
             }
 
             if (m_model_completion) {