From 3a63c3751e5414324bf0f1903b98fa793d1d3217 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 27 Apr 2020 13:27:00 -0700
Subject: [PATCH] fix #4127

---
 src/tactic/arith/purify_arith_tactic.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp
index c981cf8af..8839f99ab 100644
--- a/src/tactic/arith/purify_arith_tactic.cpp
+++ b/src/tactic/arith/purify_arith_tactic.cpp
@@ -745,7 +745,7 @@ struct purify_arith_proc {
         else {
             result = q;
             if (m_produce_proofs) {
-                r.cfg().push_cnstr_pr(nullptr);
+                r.cfg().push_cnstr_pr(m().mk_reflexivity(q));
             }
         }
     }