Addressed a bug that occurs when proof production is triggered via text flags in the input.

Separated some initialization into two phases:
1. Those that can be done when the proof compiliation flag is set
2. Those that can be done only when the --proof option is set.
For #2, deferred their execution until the text flags in the input have been processed

1 files changed, 9 insertions, 0 deletions

diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index f6f00fa11..5907f9bd5 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -130,10 +130,19 @@ public:
 
   /**
    * Ensures that a theory proof class for the given theory is created.
+   * This method can be invoked regardless of whether the "proof" option
+   * has been set.
    *
    * @param theory
    */
   void registerTheory(theory::Theory* theory);
+  /**
+   * Additional configuration of the theory proof class for the given theory.
+   * This method should only be invoked when the "proof" option has been set.
+   *
+   * @param theory
+   */
+  void finishRegisterTheory(theory::Theory* theory);
 
   theory::TheoryId getTheoryForLemma(const prop::SatClause* clause);
   TheoryProof* getTheoryProof(theory::TheoryId id);