Minor

ajreynol · Dec 20, 2024 · 1502035 · 1502035
1 parent be2a827
commit 1502035
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/rewriter/rewrite_db_proof_cons.cpp b/src/rewriter/rewrite_db_proof_cons.cpp
@@ -293,6 +293,8 @@ Node RewriteDbProofCons::preprocessClosureEq(CDProof* cdp,
       Assert(aiu != ai);
       Node eqq = ai.eqNode(aiu);
       cdp->addTheoryRewriteStep(eqq, ProofRewriteRule::QUANT_UNUSED_VARS);
+      // remains to prove the result of removing variables is equal to
+      // the right hand side.
       eq = aiu.eqNode(bi);
       cdp->addStep(eqConv, ProofRule::TRANS, {eqq, eq}, {});
     }