diff options
Diffstat (limited to 'src/util/resource_manager.cpp')
-rw-r--r-- | src/util/resource_manager.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index 2aca55616..b0fd37fd2 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -184,10 +184,10 @@ void ResourceManager::spendResource() throw (UnsafeInterruptException) { Trace("limit") << "ResourceManager::spendResource: elapsed time" << d_cumulativeTimer.elapsed() << std::endl; } - if (smt::smtEngineInScope()) { - theory::Rewriter::clearCaches(); - } if (d_isHardLimit) { + if (smt::smtEngineInScope()) { + theory::Rewriter::clearCaches(); + } throw UnsafeInterruptException(); } |