diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 21 |
1 files changed, 4 insertions, 17 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ff5cff5b6..d80c01035 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -727,16 +727,7 @@ void SmtEngine::finishInit() } if (options::perCallMillisecondLimit() != 0) { - d_resourceManager->setTimeLimit(options::perCallMillisecondLimit(), false); - } - if (options::cumulativeMillisecondLimit() != 0) - { - d_resourceManager->setTimeLimit(options::cumulativeMillisecondLimit(), - true); - } - if (options::cpuTime()) - { - d_resourceManager->useCPUTime(true); + d_resourceManager->setTimeLimit(options::perCallMillisecondLimit()); } // set the random seed @@ -3430,8 +3421,9 @@ void SmtEngine::interrupt() void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) { d_resourceManager->setResourceLimit(units, cumulative); } -void SmtEngine::setTimeLimit(unsigned long milis, bool cumulative) { - d_resourceManager->setTimeLimit(milis, cumulative); +void SmtEngine::setTimeLimit(unsigned long milis) +{ + d_resourceManager->setTimeLimit(milis); } unsigned long SmtEngine::getResourceUsage() const { @@ -3447,11 +3439,6 @@ unsigned long SmtEngine::getResourceRemaining() const return d_resourceManager->getResourceRemaining(); } -unsigned long SmtEngine::getTimeRemaining() const -{ - return d_resourceManager->getTimeRemaining(); -} - NodeManager* SmtEngine::getNodeManager() const { return d_exprManager->getNodeManager(); |