Disable nonclausal simplification for QF_SAT benchmarks by default.

(Can be overridden with --simplification=batch, for example.)

2 files changed, 6 insertions, 0 deletions

diff --git a/src/util/options.cpp b/src/util/options.cpp
index f9ab0b480..175b7f228 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -78,6 +78,7 @@ Options::Options() :
   lazyDefinitionExpansion(false),
   printWinner(false),
   simplificationMode(SIMPLIFICATION_MODE_BATCH),
+  simplificationModeSetByUser(false),
   doStaticLearning(true),
   interactive(false),
   interactiveSetByUser(false),
@@ -674,10 +675,13 @@ throw(OptionException) {
     case SIMPLIFICATION_MODE:
       if(!strcmp(optarg, "batch")) {
         simplificationMode = SIMPLIFICATION_MODE_BATCH;
+        simplificationModeSetByUser = true;
       } else if(!strcmp(optarg, "incremental")) {
         simplificationMode = SIMPLIFICATION_MODE_INCREMENTAL;
+        simplificationModeSetByUser = true;
       } else if(!strcmp(optarg, "none")) {
         simplificationMode = SIMPLIFICATION_MODE_NONE;
+        simplificationModeSetByUser = true;
       } else if(!strcmp(optarg, "help")) {
         puts(simplificationHelp.c_str());
         exit(1);
diff --git a/src/util/options.h b/src/util/options.h
index 6b8054a13..cdcefa14f 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -123,6 +123,8 @@ struct CVC4_PUBLIC Options {
 
   /** When/whether to perform nonclausal simplifications. */
   SimplificationMode simplificationMode;
+  /** Whether the user set the nonclausal simplification mode. */
+  bool simplificationModeSetByUser;
 
   /** Whether to perform the static learning pass. */
   bool doStaticLearning;