From 809b0ebca76e6ea9c03c4bc362ce4295526f6e3d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 24 Jul 2019 11:24:01 -0700
Subject: [PATCH] revert fix to #2417

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/bv_rewriter.cpp     | 4 +++-
 src/ast/rewriter/poly_rewriter_def.h | 7 +++++--
 src/model/model_evaluator.cpp        | 2 +-
 3 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 7dabd19c4..d8d34ad65 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -2084,8 +2084,10 @@ br_status bv_rewriter::mk_bv_comp(expr * arg1, expr * arg2, expr_ref & result) {
 
 br_status bv_rewriter::mk_bv_add(unsigned num_args, expr * const * args, expr_ref & result) {
     br_status st = mk_add_core(num_args, args, result);
-    if (st != BR_FAILED && st != BR_DONE)
+    if (st != BR_FAILED && st != BR_DONE) {
+        TRACE("bv", tout << result << "\n";);
         return st;
+    }
 #if 0
     expr * x;
     expr * y;
diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h
index ffe721fad..55b7348ee 100644
--- a/src/ast/rewriter/poly_rewriter_def.h
+++ b/src/ast/rewriter/poly_rewriter_def.h
@@ -1017,8 +1017,11 @@ bool poly_rewriter<Config>::hoist_ite(expr_ref& e) {
                         bs.push_back(s);
                     }
                 }
-                adds[i] = mk_add_app(bs.size(), bs.c_ptr());
-                pinned.push_back(adds[i]);
+                expr* a2 = mk_add_app(bs.size(), bs.c_ptr()); 
+                if (a != a2) {
+                    adds[i] = a2;
+                    pinned.push_back(a2);
+                }
             }
         }
         ++i;
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 1b7c54bde..50f8bde8a 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -146,7 +146,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
         bool is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f);
         br_status st = BR_FAILED;
         TRACE("model_evaluator", tout << f->get_name() << " " << is_uninterp << "\n";);        
-        if (num == 0 && (fid == null_family_id || is_uninterp || m_ar.is_as_array(f))) {
+        if (num == 0 && (fid == null_family_id || is_uninterp)) { // || m_ar.is_as_array(f)
             expr * val = m_model.get_const_interp(f);
             if (val != nullptr) {
                 result = val;