From a8dd649cc52d0870d2c62070c17a88373f681e1e Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 27 Oct 2020 17:16:06 +0100 Subject: 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. --- src/options/arith_options.toml | 2 +- src/smt/set_defaults.cpp | 10 ++++++++-- 2 files changed, 9 insertions(+), 3 deletions(-) (limited to 'src') 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 } -- cgit v1.2.3