From 94539c0d04c67f739896ef513921f2541a783d60 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 6 Apr 2020 19:49:37 -0700 Subject: [PATCH] fix #3804 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/rewriter_def.h | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index ecead81de..6a7433063 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -554,8 +554,13 @@ void rewriter_tpl::process_quantifier(quantifier * q, frame & fr) { m_pr = nullptr; if (q != new_q) { m_pr = result_pr_stack().get(fr.m_spos); - m_pr = m().mk_bind_proof(q, m_pr); - m_pr = m().mk_quant_intro(q, new_q, m_pr); + if (m_pr) { + m_pr = m().mk_bind_proof(q, m_pr); + m_pr = m().mk_quant_intro(q, new_q, m_pr); + } + else { + m_pr = m().mk_rewrite(q, new_q); + } } m_r = new_q; proof_ref pr2(m());