1 files changed, 6 insertions, 6 deletions
diff --git a/src/util/options.cpp b/src/util/options.cpp
index f68b64ab6..337eba9b6 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -82,7 +82,7 @@ Options::Options() :
   replayFilename(""),
   replayStream(NULL),
   replayLog(NULL),
-  rewriteArithEqualities(false),
+  variableRemovalEnabled(false),
   arithPropagation(false),
   satRandomFreq(0.0),
   satRandomSeed(91648253),// Minisat's default value
@@ -123,7 +123,7 @@ static const string optionsDescription = "\
    --pivot-rule=RULE      change the pivot rule (see --pivot-rule help)\n\
    --random-freq=P        sets the frequency of random decisions in the sat solver(P=0.0 by default)\n\
    --random-seed=S        sets the random seed for the sat solver\n\
-   --rewrite-arithmetic-equalities rewrite (= x y) to (and (<= x y) (>= x y)) in arithmetic\n\
+   --variable-removal-enables enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\
    --enable-arithmetic-propagation turns on arithmetic propagation\n\
    --incremental          enable incremental solving\n";
 
@@ -213,7 +213,7 @@ enum OptionValue {
   PIVOT_RULE,
   RANDOM_FREQUENCY,
   RANDOM_SEED,
-  REWRITE_ARITHMETIC_EQUALITIES,
+  ENABLE_VARIABLE_REMOVAL,
   ARITHMETIC_PROPAGATION
 };/* enum OptionValue */
 
@@ -282,7 +282,7 @@ static struct option cmdlineOptions[] = {
   { "pivot-rule" , required_argument, NULL, PIVOT_RULE  },
   { "random-freq" , required_argument, NULL, RANDOM_FREQUENCY  },
   { "random-seed" , required_argument, NULL, RANDOM_SEED  },
-  { "rewrite-arithmetic-equalities", no_argument, NULL, REWRITE_ARITHMETIC_EQUALITIES },
+  { "enable-variable-removel", no_argument, NULL, ENABLE_VARIABLE_REMOVAL },
   { "enable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION },
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
@@ -532,8 +532,8 @@ throw(OptionException) {
 #endif /* CVC4_REPLAY */
       break;
 
-    case REWRITE_ARITHMETIC_EQUALITIES:
-      rewriteArithEqualities = true;
+    case ENABLE_VARIABLE_REMOVAL:
+      variableRemovalEnabled = true;
       break;
 
     case ARITHMETIC_PROPAGATION: