diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-10-27 17:16:06 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-27 17:16:06 +0100 |
commit | a8dd649cc52d0870d2c62070c17a88373f681e1e (patch) | |
tree | 9a8cc6448a2571c536c990e082e19a63832926da /src | |
parent | b9c38b2a878841a1288b1e2279b1ecb74727eeab (diff) |
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.
Diffstat (limited to 'src')
-rw-r--r-- | src/options/arith_options.toml | 2 | ||||
-rw-r--r-- | src/smt/set_defaults.cpp | 10 |
2 files changed, 9 insertions, 3 deletions
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 } |