diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h
index 0800b6af3..7298a0e47 100644
--- a/src/ast/array_decl_plugin.h
+++ b/src/ast/array_decl_plugin.h
@@ -149,6 +149,7 @@ public:
     bool is_store(expr* n) const { return is_app_of(n, m_fid, OP_STORE); }
     bool is_const(expr* n) const { return is_app_of(n, m_fid, OP_CONST_ARRAY); }
     bool is_ext(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_EXT); }
+    bool is_ext(func_decl const* f) const { return is_decl_of(f, m_fid, OP_ARRAY_EXT); }
     bool is_map(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_MAP); }
     bool is_union(expr* n) const { return is_app_of(n, m_fid, OP_SET_UNION); }
     bool is_intersect(expr* n) const { return is_app_of(n, m_fid, OP_SET_INTERSECT); }
diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h
index 1c2935c99..31bdba4a1 100644
--- a/src/sat/smt/array_solver.h
+++ b/src/sat/smt/array_solver.h
@@ -254,6 +254,7 @@ namespace array {
         void new_diseq_eh(euf::th_eq const& eq) override;
         bool unit_propagate() override;
         void init_model() override;
+        bool include_func_interp(func_decl* f) const override { return a.is_ext(f); }
         void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
         bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
         sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index 9540cd016..ffc00a19f 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -273,7 +273,6 @@ namespace euf {
     void solver::display_validation_failure(std::ostream& out, model& mdl, enode* n) {
         out << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(n->get_expr()) << "\n";
         s().display(out);
-        return;
         euf::enode_vector nodes;
         nodes.push_back(n);
         for (unsigned i = 0; i < nodes.size(); ++i) {
@@ -327,9 +326,7 @@ namespace euf {
             CTRACE("euf", first, display_validation_failure(tout, mdl, n););
             (void)first;
             first = false;
-            return;
             exit(1);
-            first = false;
         }        
     }