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, 13 insertions, 1 deletions

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) {