Remove HOL/fmf bound messages in set defaults (#7487)

This block is misleading after the last commit.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 2ea4987ec50d3d2bcd25c5aa412503e4c05f69df..0688810cd57d92613913942f4ae5e7e661e533ff 100644 (file)
--- 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)
   {