diff options
-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(); |