From 67903280f8fe6946a36ef9fc08bfc747f74bfbd7 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Wed, 6 Jun 2012 21:11:37 +0000
Subject: [PATCH] Don't ever call nonclausalSimplify if simplificationMode =
 NONE (even if repeatSimp is true)

---
 src/smt/smt_engine.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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();
-- 
2.30.2