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)); } } }