Fix sine symmetry proof (#7783)

This PR fixes an issue in proofs for sine symmetry arising from the proof checker no longer using the rewriter.

diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index 583a54a51344a9895215abf76b125b9364c653ae..338e37baa24239828c7688e6148d94757bcc88e1 100644 (file)
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -143,7 +143,17 @@ void SineSolver::checkInitialRefine()
           if (d_data->isProofEnabled())
           {
             proof = d_data->getProof();
-            proof->addStep(lem, PfRule::ARITH_TRANS_SINE_SYMMETRY, {}, {t[0]});
+            Node tmplem =
+                nm->mkNode(Kind::PLUS,
+                           t,
+                           nm->mkNode(
+                               Kind::SINE,
+                               nm->mkNode(Kind::MULT, d_data->d_neg_one, t[0])))
+                    .eqNode(d_data->d_zero);
+            proof->addStep(
+                tmplem, PfRule::ARITH_TRANS_SINE_SYMMETRY, {}, {t[0]});
+            proof->addStep(
+                lem, PfRule::MACRO_SR_PRED_TRANSFORM, {tmplem}, {lem});
           }
           d_data->d_im.addPendingLemma(
               lem, InferenceId::ARITH_NL_T_INIT_REFINE, proof);