Fix default setting of CegisUnif options (#2605)

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index c844a197dad860469f8b3d773d6c081252c4d32c..2e52525290c400f96aa3ec9e1d2c7854941ead63 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -994,7 +994,7 @@ header = "options/quantifiers_options.h"
 [[option]]
   name       = "sygusUnifCondIndNoRepeatSol"
   category   = "regular"
-  long       = "sygus-unif-cond-indpendent-no-repeat-sol"
+  long       = "sygus-unif-cond-independent-no-repeat-sol"
   type       = "bool"
   default    = "true"
   help       = "Do not try repeated solutions when using independent synthesis of conditions in unification-based function synthesis"

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1bde3975ea13d23ce044deb0ac67cf9688fda3e1..0a48599719b33beb6957bf528992d2ab1d04bc6f 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1115,18 +1115,6 @@ void SmtEngine::setDefaults() {
   if (options::inputLanguage() == language::input::LANG_SYGUS)
   {
     is_sygus = true;
-    // must use Ferrante/Rackoff for real arithmetic
-    if (!options::cbqiMidpoint.wasSetByUser())
-    {
-      options::cbqiMidpoint.set(true);
-    }
-    if (options::sygusRepairConst())
-    {
-      if (!options::cbqi.wasSetByUser())
-      {
-        options::cbqi.set(true);
-      }
-    }
   }
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
@@ -1812,6 +1800,28 @@ void SmtEngine::setDefaults() {
     {
       options::ceGuidedInst.set(true);
     }
+    // must use Ferrante/Rackoff for real arithmetic
+    if (!options::cbqiMidpoint.wasSetByUser())
+    {
+      options::cbqiMidpoint.set(true);
+    }
+    if (options::sygusRepairConst())
+    {
+      if (!options::cbqi.wasSetByUser())
+      {
+        options::cbqi.set(true);
+      }
+    }
+    // setting unif requirements
+    if (options::sygusUnifBooleanHeuristicDt()
+        && !options::sygusUnifCondIndependent())
+    {
+      options::sygusUnifCondIndependent.set(true);
+    }
+    if (options::sygusUnifCondIndependent() && !options::sygusUnif())
+    {
+      options::sygusUnif.set(true);
+    }
   }
   if (options::sygusInference())
   {