From 8badd4ee60ed4b221ce6db55ed641544f845149c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 25 Oct 2021 12:15:43 -0500 Subject: [PATCH] Remove HOL/fmf bound messages in set defaults (#7487) This block is misleading after the last commit. --- src/smt/set_defaults.cpp | 12 ------------ 1 file changed, 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) { -- 2.30.2