Delay initialization of theory engine (#2621)

This implements solution number 2 for issue #2613.

4 files changed, 17 insertions, 0 deletions

diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index 7661c08b5..d81406dac 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -109,6 +109,11 @@ public:
     d_outputChannel.clear();
     d_logicInfo.lock();
 
+    // Notice that this unit test uses the theory engine of a created SMT
+    // engine d_smt. We must ensure that d_smt is properly initialized via
+    // the following call, which constructs its underlying theory engine.
+    d_smt->finalOptionsAreSet();
+
     // guard against duplicate statistics assertion errors
     delete d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH];
     delete d_smt->d_theoryEngine->d_theoryOut[THEORY_ARITH];
diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h
index bc5b36a0b..9b0d56998 100644
--- a/test/unit/theory/theory_bv_white.h
+++ b/test/unit/theory/theory_bv_white.h
@@ -70,6 +70,10 @@ public:
   void testBitblasterCore() {
     d_smt->setOption("bitblast", SExpr("eager"));
     d_smt->setOption("incremental", SExpr("false"));
+    // Notice that this unit test uses the theory engine of a created SMT
+    // engine d_smt. We must ensure that d_smt is properly initialized via
+    // the following call, which constructs its underlying theory engine.
+    d_smt->finalOptionsAreSet();
     EagerBitblaster* bb = new EagerBitblaster(
         dynamic_cast<TheoryBV*>(
             d_smt->d_theoryEngine->d_theoryTable[THEORY_BV]),
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 620fcd92e..50057f9fd 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -251,6 +251,10 @@ public:
 
     d_nullChannel = new FakeOutputChannel();
 
+    // Notice that this unit test uses the theory engine of a created SMT
+    // engine d_smt. We must ensure that d_smt is properly initialized via
+    // the following call, which constructs its underlying theory engine.
+    d_smt->finalOptionsAreSet();
     d_theoryEngine = d_smt->d_theoryEngine;
     for(TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id) {
       delete d_theoryEngine->d_theoryOut[id];
diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index c8265a755..4ff11014b 100644
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -166,6 +166,10 @@ class TheoryBlack : public CxxTest::TestSuite {
     d_logicInfo = new LogicInfo();
     d_logicInfo->lock();
 
+    // Notice that this unit test uses the theory engine of a created SMT
+    // engine d_smt. We must ensure that d_smt is properly initialized via
+    // the following call, which constructs its underlying theory engine.
+    d_smt->finalOptionsAreSet();
     // guard against duplicate statistics assertion errors
     delete d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN];
     delete d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN];