fix #4127

Z3Prover · Apr 27, 2020 · 3a63c37 · 3a63c37
1 parent 8996e81
commit 3a63c37
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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));
             }
         }
     }