diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index f72485d0e..cd59014aa 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -32,6 +32,7 @@ namespace smt {
     model_checker::model_checker(ast_manager & m, qi_params const & p, model_finder & mf):
         m(m),
         m_params(p),
+        m_autil(m),
         m_qm(0),
         m_context(0),
         m_root2value(0),
@@ -205,13 +206,13 @@ namespace smt {
     }
 
     void model_checker::operator()(expr *n) {
-        if (m.is_model_value(n)) {
+        if (m.is_model_value(n) || m_autil.is_as_array(n)) {
             throw is_model_value();
         }
     }
 
     bool model_checker::contains_model_value(expr* n) {
-        if (m.is_model_value(n)) {
+        if (m.is_model_value(n) || m_autil.is_as_array(n)) {
             return true;
         }
         if (is_app(n) && to_app(n)->get_num_args() == 0) {
diff --git a/src/smt/smt_model_checker.h b/src/smt/smt_model_checker.h
index 778f913c3..dd63940b7 100644
--- a/src/smt/smt_model_checker.h
+++ b/src/smt/smt_model_checker.h
@@ -22,6 +22,7 @@ Revision History:
 #define SMT_MODEL_CHECKER_H_
 
 #include "ast/ast.h"
+#include "ast/array_decl_plugin.h"
 #include "util/obj_hashtable.h"
 #include "smt/params/qi_params.h"
 #include "smt/params/smt_params.h"
@@ -39,6 +40,7 @@ namespace smt {
     class model_checker {
         ast_manager &                               m; // _manager;
         qi_params const &                           m_params;
+        array_util                                  m_autil;
         // copy of smt_params for auxiliary context.
         // the idea is to use a different configuration for the aux context (e.g., disable relevancy)
         scoped_ptr<smt_params>                      m_fparams;
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 0536c200d..11202d58a 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -643,12 +643,8 @@ namespace smt {
                 return t_result;
             }
 
-            bool is_infinite(sort * s) const {
-                // we should not assume that uninterpreted sorts are infinite in benchmarks with quantifiers.
-                return 
-                    !m.is_uninterp(s) &&
-                    s->is_infinite();
-            }
+            // we should not assume that uninterpreted sorts are infinite in benchmarks with quantifiers.
+            bool is_infinite(sort * s) const { return !m.is_uninterp(s) && s->is_infinite(); }
 
             /**
                \brief Return a fresh constant k that is used as a witness for elements that must be different from
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 1d58e2bb3..c6f83c611 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -127,10 +127,8 @@ namespace smt {
                         out << " #" << bindings[i]->get_owner_id();
                     }
                     out << " ;";
-                    ptr_vector<enode>::const_iterator it  = used_enodes.begin();
-                    ptr_vector<enode>::const_iterator end = used_enodes.end();
-                    for (; it != end; ++it)
-                        out << " #" << (*it)->get_owner_id();
+                    for (enode* n : used_enodes) 
+                        out << " #" << n->get_owner_id();
                     out << "\n";
                 }
                 m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO
@@ -150,10 +148,7 @@ namespace smt {
 
         void init_search_eh() {
             m_num_instances = 0;
-            ptr_vector<quantifier>::iterator it2  = m_quantifiers.begin();
-            ptr_vector<quantifier>::iterator end2 = m_quantifiers.end();
-            for (; it2 != end2; ++it2) {
-                quantifier * q = *it2;
+            for (quantifier * q : m_quantifiers) {
                 get_stat(q)->reset_num_instances_curr_search();
             }
             m_qi_queue.init_search_eh();