1 files changed, 8 insertions, 7 deletions

diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h
index f2784ed89..66710cd7b 100644
--- a/src/theory/arith/inference_manager.h
+++ b/src/theory/arith/inference_manager.h
@@ -37,7 +37,7 @@ class TheoryArith;
  * arithmetic theory.
  *
  * It adds some convenience methods to send ArithLemma and adds a mechanism for
- * waiting lemmas that can be flushed into the pending lemmas of the this
+ * waiting lemmas that can be flushed into the pending lemmas of this
  * buffered inference manager.
  * It also extends the caching mechanism of TheoryInferenceManager to cache
  * preprocessing lemmas and non-preprocessing lemmas separately. For the former,
@@ -51,29 +51,30 @@ class InferenceManager : public InferenceManagerBuffered
   InferenceManager(TheoryArith& ta, ArithState& astate, ProofNodeManager* pnm);
 
   /**
-   * Add a lemma as pending lemma to the this inference manager.
+   * Add a lemma as pending lemma to this inference manager.
    * If isWaiting is true, the lemma is first stored as waiting lemma and only
    * added as pending lemma when calling flushWaitingLemmas.
    */
   void addPendingArithLemma(std::unique_ptr<ArithLemma> lemma,
                             bool isWaiting = false);
   /**
-   * Add a lemma as pending lemma to the this inference manager.
+   * Add a lemma as pending lemma to this inference manager.
    * If isWaiting is true, the lemma is first stored as waiting lemma and only
    * added as pending lemma when calling flushWaitingLemmas.
    */
   void addPendingArithLemma(const ArithLemma& lemma, bool isWaiting = false);
   /**
-   * Add a lemma as pending lemma to the this inference manager.
+   * Add a lemma as pending lemma to this inference manager.
    * If isWaiting is true, the lemma is first stored as waiting lemma and only
    * added as pending lemma when calling flushWaitingLemmas.
    */
   void addPendingArithLemma(const Node& lemma,
                             InferenceId inftype,
+                            ProofGenerator* pg = nullptr,
                             bool isWaiting = false);
 
   /**
-   * Flush all waiting lemmas to the this inference manager (as pending
+   * Flush all waiting lemmas to this inference manager (as pending
    * lemmas). To actually send them, call doPendingLemmas() afterwards.
    */
   void flushWaitingLemmas();
@@ -84,8 +85,8 @@ class InferenceManager : public InferenceManagerBuffered
   void clearWaitingLemmas();
 
   /**
-   * Checks whether we have made any progress, that is whether a conflict, lemma
-   * or fact was added or whether a lemma or fact is pending.
+   * Checks whether we have made any progress, that is whether a conflict,
+   * lemma or fact was added or whether a lemma or fact is pending.
    */
   bool hasUsed() const;