fix #4127

NikolajBjorner · NikolajBjorner · commit 3a63c3751e54 · 2020-04-27T13:27:00.000-07:00
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));
             }
         }
     }

Original file line number	Diff line number	Diff line change
`@@ -745,7 +745,7 @@ struct purify_arith_proc {`
`745`	`745`	`else {`
`746`	`746`	`result = q;`
`747`	`747`	`if (m_produce_proofs) {`
`748`		`- r.cfg().push_cnstr_pr(nullptr);`
	`748`	`+ r.cfg().push_cnstr_pr(m().mk_reflexivity(q));`
`749`	`749`	`}`
`750`	`750`	`}`
`751`	`751`	`}`