diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-22 18:04:48 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-22 18:04:59 -0400 |
commit | ab38090c92343c0f1b51ebe3c4bde67c19be9253 (patch) | |
tree | a989eee14cbdc97f16938f62e81d6cc89683db46 /src/smt | |
parent | f76b86fac5da035de8531fddbd6a694103b3efaf (diff) |
One small thing forgotten in core commit.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
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; |