From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Tue, 27 Oct 2020 16:16:06 +0000 (+0100)
Subject: Disable --nl-cad option by default (#5350)
X-Git-Tag: cvc5-1.0.0~2658
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a8dd649cc52d0870d2c62070c17a88373f681e1e;p=cvc5.git

Disable --nl-cad option by default (#5350)

This PR disables the `--nl-cad` option by default. It was erroneously enabled with #5345 but leads to errors on, e.g., QF_NIA. Enabling for QF_NRA is done in set_defaults.
---

diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index f99c8df90..20ae73fce 100644
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -563,7 +563,7 @@ header = "options/arith_options.h"
   category   = "regular"
   long       = "nl-cad"
   type       = "bool"
-  default    = "true"
+  default    = "false"
   help       = "whether to use the cylindrical algebraic decomposition solver for non-linear arithmetic"
 
 [[option]]
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 7a206e2aa..0c2d06f1d 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -1444,8 +1444,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     if (!options::nlCad() && !options::nlCad.wasSetByUser())
     {
       options::nlCad.set(true);
-      options::nlExt.set(false);
-      options::nlRlvMode.set(options::NlRlvMode::INTERLEAVE);
+      if (!options::nlExt.wasSetByUser())
+      {
+        options::nlExt.set(false);
+      }
+      if (!options::nlRlvMode.wasSetByUser())
+      {
+        options::nlRlvMode.set(options::NlRlvMode::INTERLEAVE);
+      }
     }
 #endif
   }