summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r--src/smt/smt_engine.cpp18
1 files changed, 8 insertions, 10 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2bfb8353f..081e36953 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -877,8 +877,7 @@ SmtEngine::SmtEngine(ExprManager* em)
d_replayStream(NULL),
d_private(NULL),
d_statisticsRegistry(NULL),
- d_stats(NULL),
- d_channels(new LemmaChannels())
+ d_stats(NULL)
{
SmtScope smts(this);
d_originalOptions.copyValues(em->getOptions());
@@ -913,8 +912,7 @@ void SmtEngine::finishInit()
d_theoryEngine = new TheoryEngine(d_context,
d_userContext,
d_private->d_iteRemover,
- const_cast<const LogicInfo&>(d_logic),
- d_channels);
+ const_cast<const LogicInfo&>(d_logic));
// Add the theories
for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
@@ -941,9 +939,12 @@ void SmtEngine::finishInit()
d_decisionEngine->init(); // enable appropriate strategies
Trace("smt-debug") << "Making prop engine..." << std::endl;
- d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context,
- d_userContext, d_private->getReplayLog(),
- d_replayStream, d_channels);
+ d_propEngine = new PropEngine(d_theoryEngine,
+ d_decisionEngine,
+ d_context,
+ d_userContext,
+ d_private->getReplayLog(),
+ d_replayStream);
Trace("smt-debug") << "Setting up theory engine..." << std::endl;
d_theoryEngine->setPropEngine(d_propEngine);
@@ -1107,9 +1108,6 @@ SmtEngine::~SmtEngine()
delete d_context;
d_context = NULL;
- delete d_channels;
- d_channels = NULL;
-
} catch(Exception& e) {
Warning() << "CVC4 threw an exception during cleanup." << endl
<< e << endl;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback