From be4df46f6f9f48034f35578aa5110df5de5992a8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 7 Sep 2021 06:42:24 +0200
Subject: [PATCH] #5532 remove unsound rewrite rule that was recently added

---
 src/ast/rewriter/array_rewriter.cpp |  6 ------
 src/model/model_evaluator.cpp       |  3 +--
 src/sat/smt/euf_model.cpp           | 14 +++++++++++++-
 3 files changed, 14 insertions(+), 9 deletions(-)

diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp
index 39bb8f937..c25ae1156 100644
--- a/src/ast/rewriter/array_rewriter.cpp
+++ b/src/ast/rewriter/array_rewriter.cpp
@@ -693,12 +693,6 @@ br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result)
     if (m_util.is_const(rhs) && m_util.is_store(lhs)) {
         std::swap(lhs, rhs);
     }
-    if (m_util.is_const(lhs, v) && m_util.is_store(rhs)) {
-        unsigned n = to_app(rhs)->get_num_args();
-        result = m().mk_and(m().mk_eq(lhs, to_app(rhs)->get_arg(0)),
-                            m().mk_eq(v, to_app(rhs)->get_arg(n - 1)));
-        return BR_REWRITE2;
-    }
     if (m_util.is_const(lhs, v) && m_util.is_const(rhs, w)) {
         result = m().mk_eq(v, w);
         return BR_REWRITE1;
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index fc28270a6..617cfe85f 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -710,11 +710,10 @@ void model_evaluator::operator()(expr * t, expr_ref & result) {
     TRACE("model_evaluator", tout << mk_ismt2_pp(t, m()) << "\n";);
     m_imp->operator()(t, result);
     m_imp->expand_stores(result);
-    TRACE("model_evaluator", tout << result << "\n";);
+    TRACE("model_evaluator", tout << "eval: " << mk_ismt2_pp(t, m()) << " --> " << result << "\n";);
 }
 
 expr_ref model_evaluator::operator()(expr * t) {
-    TRACE("model_evaluator", tout << mk_ismt2_pp(t, m()) << "\n";);
     expr_ref result(m());
     this->operator()(t, result);
     return result;
diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index 8017f3ddc..f0f455f6c 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -189,7 +189,7 @@ namespace euf {
             else {
                 IF_VERBOSE(1, verbose_stream() << "no model values created for " << mk_pp(e, m) << "\n");
             }                
-        }
+        }           
     }
 
     void solver::values2model(deps_t const& deps, model_ref& mdl) {
@@ -291,6 +291,18 @@ namespace euf {
     }
 
     void solver::validate_model(model& mdl) {
+        model_evaluator ev(mdl);
+        ev.set_model_completion(true);
+        TRACE("model",
+            for (enode* n : m_egraph.nodes()) {
+                unsigned id = n->get_root_id();
+                expr* val = m_values.get(id, nullptr);
+                if (!val)
+                    continue;
+                expr_ref mval = ev(n->get_expr());
+                if (m.is_value(mval) && val != mval)
+                    tout << "#" << bpp(n) << " := " << mk_pp(val, m) << " ~ " << mval << "\n";
+            });
         bool first = true;
         for (enode* n : m_egraph.nodes()) {
             expr* e = n->get_expr();