diff options
Diffstat (limited to 'src/smt/set_defaults.cpp')
-rw-r--r-- | src/smt/set_defaults.cpp | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 3c35c2961..1e21abc47 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -702,6 +702,16 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const // set all defaults in the quantifiers theory, which includes sygus setDefaultsQuantifiers(logic, opts); + // shared selectors are generally not good to combine with standard + // quantifier techniques e.g. E-matching + if (opts.datatypes.dtSharedSelectorsWasSetByUser) + { + if (logic.isQuantified() && !usesSygus(opts)) + { + opts.datatypes.dtSharedSelectors = false; + } + } + // until bugs 371,431 are fixed if (!opts.prop.minisatUseElimWasSetByUser) { |