From 848a8ebb98b27015ffb04cb809c68f8db6a64bd9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 22 Jul 2021 13:35:54 -0700
Subject: [PATCH] #5427

---
 src/sat/smt/array_internalize.cpp | 4 +++-
 src/sat/smt/q_eval.cpp            | 1 -
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp
index 9d5476e31..55496a729 100644
--- a/src/sat/smt/array_internalize.cpp
+++ b/src/sat/smt/array_internalize.cpp
@@ -177,6 +177,8 @@ namespace array {
         auto set_index = [&](euf::enode* arg) { if (arg->get_root() == r) is_index = true; };
         auto set_value = [&](euf::enode* arg) { if (arg->get_root() == r) is_value = true; };
 
+        if (a.is_ext(n->get_expr()))
+            return true;
         for (euf::enode* parent : euf::enode_parents(r)) {
             app* p = parent->get_app();
             unsigned num_args = parent->num_args();
@@ -193,7 +195,7 @@ namespace array {
             }
             else if (a.is_const(p)) {
                 set_value(parent->get_arg(0));
-            }
+            }            
             if (is_array + is_index + is_value > 1)
                 return true;
         }
diff --git a/src/sat/smt/q_eval.cpp b/src/sat/smt/q_eval.cpp
index 1ecc0e4ec..59d7a5f91 100644
--- a/src/sat/smt/q_eval.cpp
+++ b/src/sat/smt/q_eval.cpp
@@ -44,7 +44,6 @@ namespace q {
             unsigned lim = m_indirect_nodes.size();
             lit l = c[i];
             lbool cmp = compare(n, binding, l.lhs, l.rhs, evidence);
-            std::cout << l.sign << ": " << l.lhs << " ~~ " << l.rhs << " " << cmp << "\n";
             switch (cmp) {
             case l_false:
                 m_indirect_nodes.shrink(lim);