diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-06 21:11:37 +0000 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-06 21:11:37 +0000 |
| commit | 67903280f8fe6946a36ef9fc08bfc747f74bfbd7 (patch) | |
| tree | 4ba788f7758339a15e8377e2e7618c0811f27420 /src | |
| parent | 35dea35f309952919365ee85f991184bddfda514 (diff) | |
Don't ever call nonclausalSimplify if simplificationMode = NONE (even if
repeatSimp is true)
Diffstat (limited to 'src')
| -rw-r--r-- | src/smt/smt_engine.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index cc645f7b7..8b3e6b742 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1042,7 +1042,7 @@ void SmtEnginePrivate::simplifyAssertions() unconstrainedSimp(); } - if(Options::current()->repeatSimp) { + if(Options::current()->repeatSimp && Options::current()->simplificationMode != Options::SIMPLIFICATION_MODE_NONE) { d_assertionsToCheck.swap(d_assertionsToPreprocess); // Abuse the user context to make sure circuit propagator gets backtracked d_smt.d_userContext->push(); |