From b013df9a9f9119887a80bea32d6bbf5f1c1055f6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 4 Jun 2020 00:47:27 -0700
Subject: [PATCH] fix #4431

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/rewriter_def.h | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index bd5f4ff4a..b026b6a47 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -802,6 +802,7 @@ void rewriter_tpl<Config>::operator()(expr * t, expr_ref & result, proof_ref & r
     if (!frame_stack().empty() || m_cache != m_cache_stack[0]) {
         frame_stack().reset();
         result_stack().reset();
+        result_pr_stack().reset();
         m_scopes.reset();
         reset_cache();
     }