diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-25 12:15:43 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-25 12:15:43 -0500 |
| commit | 8badd4ee60ed4b221ce6db55ed641544f845149c (patch) | |
| tree | c1643e125e587c37e804c78009be04ca9e0f4e1b | |
| parent | 0e28a3a86f45e012e59751b0091760f5e2baebd6 (diff) | |
Remove HOL/fmf bound messages in set defaults (#7487)
This block is misleading after the last commit.
| -rw-r--r-- | src/smt/set_defaults.cpp | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 2ea4987ec..0688810cd 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -1340,18 +1340,6 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, { opts.quantifiers.macrosQuant = false; } - // HOL is incompatible with fmfBound - if (opts.quantifiers.fmfBound) - { - if (opts.quantifiers.fmfBoundWasSetByUser - || opts.quantifiers.fmfBoundLazyWasSetByUser - || opts.quantifiers.fmfBoundIntWasSetByUser) - { - Notice() << "Disabling bound finite-model finding since it is " - "incompatible with HOL.\n"; - } - Trace("smt") << "turning off fmf-bound, since HOL\n"; - } } if (opts.quantifiers.fmfFunWellDefinedRelevant) { |