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 | |
| parent | f76b86fac5da035de8531fddbd6a694103b3efaf (diff) | |
One small thing forgotten in core commit.
| -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; |