From b50da20531c83f848db7ac086120150bc623fd1a Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Wed, 30 May 2018 13:45:48 -0700
Subject: [PATCH] array_mbp: turn on model completion

---
 src/qe/qe_arrays.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp
index 1b3bd6c20..bcf642fb7 100644
--- a/src/qe/qe_arrays.cpp
+++ b/src/qe/qe_arrays.cpp
@@ -631,6 +631,7 @@ namespace qe {
         void operator () (model& mdl, app_ref_vector& arr_vars, expr_ref& fml, app_ref_vector& aux_vars) {
             reset ();
             model_evaluator mev(mdl);
+            mev.set_model_completion(true);
             M = &mdl;
             m_mev = &mev;
 
@@ -857,6 +858,7 @@ namespace qe {
 
             reset ();
             model_evaluator mev(mdl);
+            mev.set_model_completion(true);
             M = &mdl;
             m_mev = &mev;
             m_reduce_all_selects = reduce_all_selects;
@@ -1167,6 +1169,7 @@ namespace qe {
                 TRACE ("qe", tout << "Failed to project arrays\n";);
             }
 
+            mev.set_model_completion(true);
             // dealloc
             for (auto & kv : m_sel_terms) dealloc(kv.m_value);
             m_sel_terms.reset ();