[hol] Disable bound fmf when HOL (#6792)

Fixes #6536

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index e119ce4d4ce29b17b524d7909d9cce5fc39c25d6..7ae07d196e108058349f377236369a144e617997 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -296,7 +296,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     if (!opts.quantifiers.fmfBoundWasSetByUser)
     {
       opts.quantifiers.fmfBound = true;
-      Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
+      Trace("smt") << "turning on fmf-bound, for strings-exp" << std::endl;
     }
     // Note we allow E-matching by default to support combinations of sequences
     // and quantifiers.
@@ -894,7 +894,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     options::DecisionMode decMode =
         // anything that uses sygus uses internal
         usesSygus ? options::DecisionMode::INTERNAL :
-                  // ALL  or its supersets
+                  // ALL or its supersets
             logic.hasEverything()
                 ? options::DecisionMode::JUSTIFICATION
                 : (  // QF_BV
@@ -973,9 +973,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       || (opts.quantifiers.fmfBoundIntWasSetByUser && options::fmfBoundInt()))
   {
     opts.quantifiers.fmfBound = true;
+    Trace("smt")
+        << "turning on fmf-bound, for fmf-bound-int or fmf-bound-lazy\n";
   }
-  // now have determined whether fmfBoundInt is on/off
-  // apply fmfBoundInt options
+  // now have determined whether fmfBound is on/off
+  // apply fmfBound options
   if (options::fmfBound())
   {
     if (!opts.quantifiers.mbqiModeWasSetByUser
@@ -1015,6 +1017,20 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     {
       opts.quantifiers.macrosQuant = false;
     }
+    // HOL is incompatible with fmfBound
+    if (options::fmfBound())
+    {
+      if (opts.quantifiers.fmfBoundWasSetByUser
+          || opts.quantifiers.fmfBoundLazyWasSetByUser
+          || opts.quantifiers.fmfBoundIntWasSetByUser)
+      {
+        Notice() << "Disabling bound finite-model finding since it is "
+                    "incompatible with HOL.\n";
+      }
+
+      opts.quantifiers.fmfBound = false;
+      Trace("smt") << "turning off fmf-bound, since HOL\n";
+    }
   }
   if (options::fmfFunWellDefinedRelevant())
   {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index ac837b957bc1e21297ba70d2e9e6e01159730ddb..45b695cd96edab34b93a4baae32c89fc375f09cb 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -634,6 +634,7 @@ set(regress_0_tests
   regress0/ho/issue5233-part1-usort-owner.smt2
   regress0/ho/issue5371.smt2
   regress0/ho/issue6526.smt2
+  regress0/ho/issue6536.smt2
   regress0/ho/ite-apply-eq.smt2
   regress0/ho/lambda-equality-non-canon.smt2
   regress0/ho/match-middle.smt2

diff --git a/test/regress/regress0/ho/issue6536.smt2 b/test/regress/regress0/ho/issue6536.smt2
new file mode 100644 (file)
index 0000000..ed4d453
--- /dev/null
+++ b/test/regress/regress0/ho/issue6536.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unknown
+(set-logic HO_ALL)
+(declare-datatypes ((a 0) (b 0)) (((c) (d)) ((h (j b)) (e))))
+(declare-fun f () b)
+(declare-fun k (a) b)
+(declare-fun g (b b) b)
+(assert (forall ((i a)) (distinct (k i) (ite ((_ is c) i) e (ite ((_ is d) i) (h (g (k  i) (k  i))) f)))))
+(check-sat)