diff options
| -rw-r--r-- | src/theory/arith/nl/transcendental/sine_solver.cpp | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index 583a54a51..338e37baa 100644 --- 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); |