From c21cd6ffa5e477849f8a68ac330d9558886a31f9 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Fri, 7 Jun 2013 16:16:56 -0700
Subject: [PATCH] fixed model completion problem in duality

---
 src/duality/duality_wrapper.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h
index 9477ab0fa..4a6d32695 100755
--- a/src/duality/duality_wrapper.h
+++ b/src/duality/duality_wrapper.h
@@ -679,7 +679,7 @@ namespace Duality {
             return *this; 
         }
         
-        expr eval(expr const & n, bool model_completion=false) const {
+        expr eval(expr const & n, bool model_completion=true) const {
 	  ::model * _m = m_model.get();
 	  expr_ref result(ctx().m());
 	  _m->eval(n, result, model_completion);