diff options
Diffstat (limited to 'src/smt/set_defaults.cpp')
| -rw-r--r-- | src/smt/set_defaults.cpp | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index b2fe2b5d6..194290399 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -373,7 +373,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const || opts.smt.produceInterpols != options::ProduceInterpols::NONE || opts.smt.modelCoresMode != options::ModelCoresMode::NONE || opts.smt.blockModelsMode != options::BlockModelsMode::NONE - || opts.smt.produceProofs) + || opts.smt.produceProofs || isSygus(opts)) && !opts.smt.produceAssertions) { verbose(1) << "SolverEngine: turning on produce-assertions to support " @@ -807,6 +807,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const if (!opts.arith.nlCad && !opts.arith.nlCadWasSetByUser) { opts.arith.nlCad = true; + opts.arith.nlCadVarElim = true; if (!opts.arith.nlExtWasSetByUser) { opts.arith.nlExt = options::NlExtMode::LIGHT; @@ -823,6 +824,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const if (!opts.arith.nlCad && !opts.arith.nlCadWasSetByUser) { opts.arith.nlCad = true; + opts.arith.nlCadVarElim = true; if (!opts.arith.nlExtWasSetByUser) { opts.arith.nlExt = options::NlExtMode::LIGHT; @@ -1161,9 +1163,8 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts, bool SetDefaults::safeUnsatCores(const Options& opts) const { // whether we want to force safe unsat cores, i.e., if we are in the default - // ASSUMPTIONS mode or PP_ONLY, since other ones are experimental - return opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS - || opts.smt.unsatCoresMode == options::UnsatCoresMode::PP_ONLY; + // ASSUMPTIONS mode, since other ones are experimental + return opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS; } bool SetDefaults::incompatibleWithQuantifiers(Options& opts, |