From: Clark Barrett <barrett@cs.nyu.edu>
Date: Wed, 6 Jun 2012 21:11:37 +0000 (+0000)
Subject: Don't ever call nonclausalSimplify if simplificationMode = NONE (even if
X-Git-Tag: cvc5-1.0.0~8115
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=67903280f8fe6946a36ef9fc08bfc747f74bfbd7;p=cvc5.git

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