Merge branch 'master' into fixRefCountZerofixRefCountZero

1 files changed, 7 insertions, 1 deletions

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index fa4c1ecb5..bbf5b0064 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -579,9 +579,13 @@ void LFSCProof::toStream(std::ostream& out) const
     CodeTimer skeletonProofTimer{
         ProofManager::currentPM()->getStats().d_skeletonProofTraceTime};
     Assert(!d_satProof->proofConstructed());
+
+    // Here we give our SAT solver a chance to flesh out the resolution proof.
+    // It proves bottom from a set of clauses.
     d_satProof->constructProof();
 
-    // collecting leaf clauses in resolution proof
+    // We ask the SAT solver which clauses are used in that proof.
+    // For a resolution proof, these are the leaves of the tree.
     d_satProof->collectClausesUsed(used_inputs, used_lemmas);
 
     IdToSatClause::iterator it2;
@@ -672,6 +676,8 @@ void LFSCProof::toStream(std::ostream& out) const
       }
     }
 
+    // From the clauses, compute the atoms (atomic theory predicates in
+    // assertions and lemmas).
     d_cnfProof->collectAtomsForClauses(used_inputs, atoms);
     d_cnfProof->collectAtomsForClauses(used_lemmas, atoms);