Disable --nl-cad option by default (#5350)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Tue, 27 Oct 2020 16:16:06 +0000 (17:16 +0100)
committerGitHub <noreply@github.com>
Tue, 27 Oct 2020 16:16:06 +0000 (17:16 +0100)
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.

src/options/arith_options.toml
src/smt/set_defaults.cpp

index f99c8df90d83d32b764e90cbbe1709b51ffaea99..20ae73fce92840c16a1f02c47f4038cd70bdfc0b 100644 (file)
@@ -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]]
index 7a206e2aaa4c0e9cefb407338bba1cc28e4f3d6e..0c2d06f1dbabd5c407f0d03b1fdd707467daadf7 100644 (file)
@@ -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
   }