diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 80dea338a..c9416ad4e 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -1494,6 +1494,7 @@ namespace arith {
         case OP_IS_INT:
         case OP_TO_INT:
         case OP_TO_REAL:
+        case OP_NUM:
             return false;
         default:
             return true;            
diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp
index 92a368095..1f1066121 100644
--- a/src/sat/smt/array_model.cpp
+++ b/src/sat/smt/array_model.cpp
@@ -60,6 +60,11 @@ namespace array {
         ptr_vector<expr> args;
         sort* srt = n->get_sort();
         n = n->get_root();
+        if (a.is_as_array(n->get_expr())) {
+            values.set(n->get_expr_id(), n->get_expr());
+            return;
+        }
+            
         unsigned arity = get_array_arity(srt);
         func_decl * f    = mk_aux_decl_for_array_sort(m, srt);
         func_interp * fi = alloc(func_interp, m, arity);