diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp
index ac90617f3..555c1b5c2 100644
--- a/src/ast/rewriter/array_rewriter.cpp
+++ b/src/ast/rewriter/array_rewriter.cpp
@@ -644,8 +644,6 @@ bool array_rewriter::add_store(expr_ref_vector& args, unsigned num_idxs, expr* e
 bool array_rewriter::is_expandable_store(expr* s) {
     unsigned count = 0;
     unsigned depth = 0;
-    if (false && !is_ground(s))
-        return false;
     while (m_util.is_store(s)) {
         s = to_app(s)->get_arg(0);
         count += s->get_ref_count();
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index f5b568969..ee36fc1e3 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -597,6 +597,7 @@ void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
     end_scope();
     cache_result<ProofGen>(q, m_r, m_pr, fr.m_cache_result);
     m_r = nullptr;
+    m_pr = nullptr;
     frame_stack().pop_back();
     set_new_child_flag(q, m_r);
 }