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

3 files changed, 22 insertions, 2 deletions

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 45b1f046e..d61261b38 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -96,7 +96,6 @@ CnfProof* ProofManager::getCnfProof() {
 }
 
 TheoryProofEngine* ProofManager::getTheoryProofEngine() {
-  Assert (options::proof());
   Assert (currentPM()->d_theoryProof != NULL);
   return currentPM()->d_theoryProof;
 }
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 7fa11cc5f..634b2b738 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -79,7 +79,6 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) {
       if (id == theory::THEORY_BV) {
         BitVectorProof * bvp = new LFSCBitVectorProof((theory::bv::TheoryBV*)th, this);
         d_theoryProofTable[id] = bvp;
-        ((theory::bv::TheoryBV*)th)->setProofLog( bvp );
         return;
       }
 
@@ -98,6 +97,19 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) {
   }
 }
 
+void TheoryProofEngine::finishRegisterTheory(theory::Theory* th) {
+  if (th) {
+    theory::TheoryId id = th->getId();
+    if (id == theory::THEORY_BV) {
+      Assert(d_theoryProofTable.find(id) != d_theoryProofTable.end());
+
+      BitVectorProof *bvp = (BitVectorProof *)d_theoryProofTable[id];
+      ((theory::bv::TheoryBV*)th)->setProofLog( bvp );
+      return;
+    }
+  }
+}
+
 TheoryProof* TheoryProofEngine::getTheoryProof(theory::TheoryId id) {
   // The UF theory handles queries for the Builtin theory.
   if (id == theory::THEORY_BUILTIN) {
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);