Don't ever call nonclausalSimplify if simplificationMode = NONE (even if

repeatSimp is true)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index cc645f7b798868cf951335adb6f4bacb96d4f62d..8b3e6b7424b3b32e01c2308917a71a04303bfac7 100644 (file)
--- 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();