From 31164c2eaf82906a34699a2c6d6644b502d74e5f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 18 Mar 2020 10:40:34 -0700
Subject: [PATCH] fix #3386

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/qe/qe_tactic.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/qe/qe_tactic.cpp b/src/qe/qe_tactic.cpp
index 512679de0..3bc5d65f4 100644
--- a/src/qe/qe_tactic.cpp
+++ b/src/qe/qe_tactic.cpp
@@ -66,6 +66,7 @@ class qe_tactic : public tactic {
                 m_qe(m.mk_true(), f, new_f);
                 new_pr = nullptr;
                 if (produce_proofs) {
+                    new_pr = m.mk_rewrite(f, new_f);
                     new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
                 }
                 g->update(i, new_f, new_pr, g->dep(i));