diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-15 11:42:28 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-15 09:42:28 -0700 |
commit | d828df78c39000b54c2a7824482e206f6761664f (patch) | |
tree | 1c3f2f6cd119ce6bd3a9d59593d22d895801ab44 /test | |
parent | de7798ebbc351046d7b5ae7e6379ffd61be0f1c4 (diff) |
Delay initialization of theory engine (#2621)
This implements solution number 2 for issue #2613.
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/prop/cnf_stream_white.h | 4 | ||||
-rw-r--r-- | test/unit/theory/theory_arith_white.h | 5 | ||||
-rw-r--r-- | test/unit/theory/theory_bv_white.h | 4 | ||||
-rw-r--r-- | test/unit/theory/theory_engine_white.h | 4 | ||||
-rw-r--r-- | test/unit/theory/theory_white.h | 4 |
5 files changed, 21 insertions, 0 deletions
diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h index 7e04bb7c5..35eb240a2 100644 --- a/test/unit/prop/cnf_stream_white.h +++ b/test/unit/prop/cnf_stream_white.h @@ -136,6 +136,10 @@ class CnfStreamWhite : public CxxTest::TestSuite { d_nodeManager = NodeManager::fromExprManager(d_exprManager); d_scope = new SmtScope(d_smt); + // 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; d_satSolver = new FakeSatSolver(); 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]; |