From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 22 Aug 2014 22:04:48 +0000 (-0400)
Subject: One small thing forgotten in core commit.
X-Git-Tag: cvc5-1.0.0~6656
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ab38090c92343c0f1b51ebe3c4bde67c19be9253;p=cvc5.git

One small thing forgotten in core commit.
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7b1f99403..730852d4a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1753,8 +1753,11 @@ static void dumpAssertions(const char* key, const AssertionPipeline& assertionLi
 bool SmtEnginePrivate::nonClausalSimplify() {
   d_smt.finalOptionsAreSet();
 
-  TimerStat::CodeTimer nonclausalTimer(d_smt.d_stats->d_nonclausalSimplificationTime);
+  if(options::unsatCores()) {
+    return true;
+  }
 
+  TimerStat::CodeTimer nonclausalTimer(d_smt.d_stats->d_nonclausalSimplificationTime);
 
   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl;