From 5e7db2e3e2bebb3507598af710aaf28177ce4375 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 18 May 2016 08:29:24 -0700
Subject: [PATCH] disable mk_array_eq as it breaks model evaluation/validation

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

diff --git a/src/math/grobner/grobner.cpp b/src/math/grobner/grobner.cpp
index 2bf4d5ba3..0c96dfde3 100644
--- a/src/math/grobner/grobner.cpp
+++ b/src/math/grobner/grobner.cpp
@@ -249,6 +249,7 @@ void grobner::update_order() {
 }
 
 bool grobner::var_lt::operator()(expr * v1, expr * v2) const {
+    if (v1 == v2) return false;
     int w1 = 0;
     int w2 = 0;
     m_var2weight.find(v1, w1);
@@ -268,6 +269,8 @@ bool grobner::monomial_lt::operator()(monomial * m1, monomial * m2) const {
     for (; it1 != end1; ++it1, ++it2) {
         expr * v1 = *it1;
         expr * v2 = *it2;
+        if (v1 == v2)
+            continue;
         if (m_var_lt(v1, v2))
             return true;
         if (v1 != v2)
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index a5b900ab7..c83da2050 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -259,6 +259,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
 
 
     br_status mk_array_eq(expr* a, expr* b, expr_ref& result) {
+        return BR_FAILED;
+        // disabled until made more efficient
         if (a == b) {
             result = m().mk_true();
             return BR_DONE;
@@ -271,6 +273,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
             conj.push_back(m().mk_eq(else1, else2));
             args1.push_back(a);
             args2.push_back(b);
+            // TBD: this is too inefficient.
             for (unsigned i = 0; i < stores.size(); ++i) {
                 args1.resize(1); args1.append(stores[i].size() - 1, stores[i].c_ptr());
                 args2.resize(1); args2.append(stores[i].size() - 1, stores[i].c_ptr());