From 972ab6298cde5cdeade5d7f456e9738fe2c8dd6b Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Wed, 21 Jun 2017 22:59:52 -0400
Subject: [PATCH] (mev) only reduce function interpretation

---
 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 279cfde3b..805ed8e5d 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -432,6 +432,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
         func_interp* g = m_model.get_func_interp(f);
         unsigned sz = g->num_entries();
         unsigned arity = f->get_arity();
+        unsigned base_sz = stores.size();
         for (unsigned i = 0; i < sz; ++i) {
             expr_ref_vector store(m());
             func_entry const* fe = g->get_entry(i);
@@ -456,7 +457,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
             TRACE("model_evaluator", tout << "non-ground else case " << mk_pp(a, m()) << "\n" << else_case << "\n";);
             return false;
         }
-        for (unsigned i = stores.size(); are_values && i > 0; ) {
+        for (unsigned i = stores.size(); are_values && i > base_sz; ) {
             --i;
             if (m().are_equal(else_case, stores[i].back())) {
                 for (unsigned j = i + 1; j < stores.size(); ++j) {