diff options
Diffstat (limited to 'test/unit/prop/cnf_stream_black.h')
| -rw-r--r-- | test/unit/prop/cnf_stream_black.h | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index c24104acc..de0510582 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -146,6 +146,7 @@ class CnfStreamBlack : public CxxTest::TestSuite { NodeManagerScope nms(d_nodeManager); d_satSolver = new FakeSatSolver(); d_logicInfo = new LogicInfo(); + d_logicInfo->lock(); d_theoryEngine = new TheoryEngine(d_context, d_userContext, *d_logicInfo); d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(theory::THEORY_BUILTIN); d_theoryEngine->addTheory<theory::booleans::TheoryBool>(theory::THEORY_BOOL); @@ -200,9 +201,15 @@ public: TS_ASSERT( d_satSolver->addClauseCalled() ); } + void testTrue() { + NodeManagerScope nms(d_nodeManager); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false ); + TS_ASSERT( d_satSolver->addClauseCalled() ); + } + void testFalse() { NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false ); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -255,12 +262,6 @@ public: TS_ASSERT( d_satSolver->addClauseCalled() ); } - void testTrue() { - NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false ); - TS_ASSERT( d_satSolver->addClauseCalled() ); - } - void testVar() { NodeManagerScope nms(d_nodeManager); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); |