Merge branch 'master' into fix-cln-static-downloadfix-cln-static-download

24 files changed, 103 insertions, 71 deletions

diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml
index 60cdcc335..0bb0edba6 100644
--- a/src/options/datatypes_options.toml
+++ b/src/options/datatypes_options.toml
@@ -86,28 +86,40 @@ name   = "Datatypes Theory"
   help       = "internally use shared selectors across multiple constructors"
 
 [[option]]
-  name       = "sygusSymBreak"
+  name       = "sygusSimpleSymBreak"
   category   = "regular"
-  long       = "sygus-sym-break"
-  type       = "bool"
-  default    = "true"
-  help       = "simple sygus symmetry breaking lemmas"
-
-[[option]]
-  name       = "sygusSymBreakAgg"
-  category   = "regular"
-  long       = "sygus-sym-break-agg"
-  type       = "bool"
-  default    = "true"
-  help       = "use aggressive checks for simple sygus symmetry breaking lemmas"
-
-[[option]]
-  name       = "sygusSymBreakDynamic"
-  category   = "regular"
-  long       = "sygus-sym-break-dynamic"
-  type       = "bool"
-  default    = "true"
-  help       = "dynamic sygus symmetry breaking lemmas"
+  long       = "sygus-simple-sym-break=MODE"
+  type       = "SygusSimpleSymBreakMode"
+  default    = "AGG"
+  help       = "if and how to apply simple symmetry breaking based on the grammar for smart enumeration"
+  help_mode  = "Modes for applying simple symmetry breaking based on the grammar for smart enumeration."
+[[option.mode.NONE]]
+  name = "none"
+  help = "Do not apply simple symmetry breaking."
+[[option.mode.BASIC]]
+  name = "basic"
+  help = "Apply basic simple symmetry breaking."
+[[option.mode.AGG]]
+  name = "agg"
+  help = "Apply aggressive simple symmetry breaking."
+  
+[[option]]
+  name       = "sygusRewriter"
+  category   = "regular"
+  long       = "sygus-rewriter=MODE"
+  type       = "SygusRewriterMode"
+  default    = "EXTENDED"
+  help       = "if and how to apply rewriting for sygus symmetry breaking"
+  help_mode  = "Modes for applying rewriting for sygus symmetry breaking."
+[[option.mode.NONE]]
+  name = "none"
+  help = "Do not use the rewriter."
+[[option.mode.BASIC]]
+  name = "basic"
+  help = "Use the basic rewriter."
+[[option.mode.EXTENDED]]
+  name = "extended"
+  help = "Use the extended rewriter."
 
 [[option]]
   name       = "sygusSymBreakPbe"
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index c284518c7..312fc606b 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1261,14 +1261,6 @@ name   = "Quantifiers"
   help       = "enumerate a stream of solutions instead of terminating after the first one"
 
 [[option]]
-  name       = "sygusExtRew"
-  category   = "regular"
-  long       = "sygus-ext-rew"
-  type       = "bool"
-  default    = "true"
-  help       = "use extended rewriter for sygus"
-
-[[option]]
   name       = "cegisSample"
   category   = "regular"
   long       = "cegis-sample=MODE"
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 7e8a54398..7d26b4ff0 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -16,6 +16,7 @@
 #include "preprocessing/preprocessing_pass_context.h"
 
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "options/base_options.h"
 #include "smt/env.h"
 #include "theory/theory_engine.h"
@@ -85,7 +86,7 @@ std::vector<Node> PreprocessingPassContext::getLearnedLiterals() const
 void PreprocessingPassContext::printSubstitution(const Node& lhs,
                                                  const Node& rhs) const
 {
-  Node eq = lhs.eqNode(rhs);
+  Node eq = SkolemManager::getOriginalForm(lhs.eqNode(rhs));
   output(OutputTag::LEARNED_LITS)
       << "(learned-lit " << eq << " :preprocess-subs)" << std::endl;
   output(OutputTag::SUBS) << "(substitution " << eq << ")" << std::endl;
diff --git a/src/prop/zero_level_learner.cpp b/src/prop/zero_level_learner.cpp
index 1b11662aa..3562545b8 100644
--- a/src/prop/zero_level_learner.cpp
+++ b/src/prop/zero_level_learner.cpp
@@ -84,7 +84,8 @@ void ZeroLevelLearner::notifyInputFormulas(
     for (const Node& lit : ppl)
     {
       output(OutputTag::LEARNED_LITS)
-          << "(learned-lit " << lit << " :preprocess)" << std::endl;
+          << "(learned-lit " << SkolemManager::getOriginalForm(lit)
+          << " :preprocess)" << std::endl;
     }
   }
   for (const Node& a : assertions)
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index fea9d4398..1fd2c3dc5 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -1580,9 +1580,9 @@ void SetDefaults::setDefaultsSygus(Options& opts) const
     opts.quantifiers.sygusRewSynth = true;
     // we should not use the extended rewriter, since we are interested
     // in rewrites that are not in the main rewriter
-    if (!opts.quantifiers.sygusExtRewWasSetByUser)
+    if (!opts.datatypes.sygusRewriterWasSetByUser)
     {
-      opts.quantifiers.sygusExtRew = false;
+      opts.datatypes.sygusRewriter = options::SygusRewriterMode::BASIC;
     }
   }
   // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 0318f7da9..1134c0a5a 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -691,7 +691,8 @@ Node SygusExtension::getSimpleSymBreakPred(Node e,
 
   // if we are the "any constant" constructor, we do no symmetry breaking
   // only do simple symmetry breaking up to depth 2
-  bool doSymBreak = options().datatypes.sygusSymBreak;
+  bool doSymBreak = options().datatypes.sygusSimpleSymBreak
+                    != options::SygusSimpleSymBreakMode::NONE;
   if (isAnyConstant || depth > 2)
   {
     doSymBreak = false;
@@ -1047,7 +1048,7 @@ Node SygusExtension::registerSearchValue(Node a,
                             << ", type=" << tn << std::endl;
     Node bv = d_tds->sygusToBuiltin(cnv, tn);
     Trace("sygus-sb-debug") << "  ......builtin is " << bv << std::endl;
-    Node bvr = extendedRewrite(bv);
+    Node bvr = d_tds->rewriteNode(bv);
     Trace("sygus-sb-debug") << "  ......search value rewrites to " << bvr << std::endl;
     Trace("dt-sygus") << "  * DT builtin : " << n << " -> " << bvr << std::endl;
     unsigned sz = utils::getSygusTermSize(nv);
@@ -1624,7 +1625,9 @@ void SygusExtension::check()
 
         // register the search value ( prog -> progv ), this may invoke symmetry
         // breaking
-        if (!isExc && options().datatypes.sygusSymBreakDynamic)
+        if (!isExc
+            && options().datatypes.sygusRewriter
+                   != options::SygusRewriterMode::NONE)
         {
           bool isVarAgnostic = d_tds->isVariableAgnosticEnumerator(prog);
           // check that it is unique up to theory-specific rewriting and
diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
index 233d7f17b..a4b65ab30 100644
--- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
@@ -125,7 +125,7 @@ Node EnumStreamPermutation::getNext()
   {
     d_first = false;
     Node bultin_value = d_tds->sygusToBuiltin(d_value, d_value.getType());
-    d_perm_values.insert(extendedRewrite(bultin_value));
+    d_perm_values.insert(d_tds->rewriteNode(bultin_value));
     return d_value;
   }
   unsigned n_classes = d_perm_state_class.size();
@@ -192,9 +192,9 @@ Node EnumStreamPermutation::getNext()
     bultin_perm_value = d_tds->sygusToBuiltin(perm_value, perm_value.getType());
     Trace("synth-stream-concrete-debug")
         << " ......perm builtin is " << bultin_perm_value;
-    if (options().datatypes.sygusSymBreakDynamic)
+    if (options().datatypes.sygusRewriter != options::SygusRewriterMode::NONE)
     {
-      bultin_perm_value = extendedRewrite(bultin_perm_value);
+      bultin_perm_value = d_tds->rewriteNode(bultin_perm_value);
       Trace("synth-stream-concrete-debug")
           << " and rewrites to " << bultin_perm_value;
     }
@@ -512,9 +512,9 @@ Node EnumStreamSubstitution::getNext()
   // construction (unless it's equiv to a constant, e.g. true / false)
   Node builtin_comb_value =
       d_tds->sygusToBuiltin(comb_value, comb_value.getType());
-  if (options().datatypes.sygusSymBreakDynamic)
+  if (options().datatypes.sygusRewriter != options::SygusRewriterMode::NONE)
   {
-    builtin_comb_value = extendedRewrite(builtin_comb_value);
+    builtin_comb_value = d_tds->rewriteNode(builtin_comb_value);
   }
   if (Trace.isOn("synth-stream-concrete"))
   {
diff --git a/src/theory/quantifiers/sygus/enum_value_manager.cpp b/src/theory/quantifiers/sygus/enum_value_manager.cpp
index fcbe3d42e..d9078bfaf 100644
--- a/src/theory/quantifiers/sygus/enum_value_manager.cpp
+++ b/src/theory/quantifiers/sygus/enum_value_manager.cpp
@@ -100,7 +100,8 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete)
                || options().quantifiers.sygusEnumMode
                       == options::SygusEnumMode::AUTO);
         // create the enumerator callback
-        if (options().datatypes.sygusSymBreakDynamic)
+        if (options().datatypes.sygusRewriter
+            != options::SygusRewriterMode::NONE)
         {
           std::ostream* out = nullptr;
           if (options().quantifiers.sygusRewVerify)
@@ -112,7 +113,7 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete)
             out = options().base.out;
           }
           d_secd = std::make_unique<SygusEnumeratorCallbackDefault>(
-              d_env, e, &d_stats, d_eec.get(), d_samplerRrV.get(), out);
+              d_env, e, d_tds, &d_stats, d_eec.get(), d_samplerRrV.get(), out);
         }
         // if sygus repair const is enabled, we enumerate terms with free
         // variables as arguments to any-constant constructors
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index 52c1ef4a0..ba4496a7b 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -55,10 +55,11 @@ void SygusEnumerator::initialize(Node e)
   Trace("sygus-enum") << "SygusEnumerator::initialize " << e << std::endl;
   d_enum = e;
   // allocate the default callback
-  if (d_sec == nullptr && options().datatypes.sygusSymBreakDynamic)
+  if (d_sec == nullptr
+      && options().datatypes.sygusRewriter != options::SygusRewriterMode::NONE)
   {
-    d_secd =
-        std::make_unique<SygusEnumeratorCallbackDefault>(d_env, e, d_stats);
+    d_secd = std::make_unique<SygusEnumeratorCallbackDefault>(
+        d_env, e, d_tds, d_stats);
     d_sec = d_secd.get();
   }
   d_etype = d_enum.getType();
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp
index bde1fdd67..d16b6d33e 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp
@@ -18,6 +18,7 @@
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/sygus/example_eval_cache.h"
 #include "theory/quantifiers/sygus/sygus_stats.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/sygus_sampler.h"
 #include "theory/rewriter.h"
 
@@ -27,8 +28,9 @@ namespace quantifiers {
 
 SygusEnumeratorCallback::SygusEnumeratorCallback(Env& env,
                                                  Node e,
+                                                 TermDbSygus* tds,
                                                  SygusStatistics* s)
-    : EnvObj(env), d_enum(e), d_stats(s)
+    : EnvObj(env), d_enum(e), d_tds(tds), d_stats(s)
 {
   d_tn = e.getType();
 }
@@ -36,7 +38,7 @@ SygusEnumeratorCallback::SygusEnumeratorCallback(Env& env,
 bool SygusEnumeratorCallback::addTerm(Node n, std::unordered_set<Node>& bterms)
 {
   Node bn = datatypes::utils::sygusToBuiltin(n);
-  Node bnr = extendedRewrite(bn);
+  Node bnr = d_tds == nullptr ? extendedRewrite(bn) : d_tds->rewriteNode(bn);
   if (d_stats != nullptr)
   {
     ++(d_stats->d_enumTermsRewrite);
@@ -66,11 +68,12 @@ bool SygusEnumeratorCallback::addTerm(Node n, std::unordered_set<Node>& bterms)
 SygusEnumeratorCallbackDefault::SygusEnumeratorCallbackDefault(
     Env& env,
     Node e,
+    TermDbSygus* tds,
     SygusStatistics* s,
     ExampleEvalCache* eec,
     SygusSampler* ssrv,
     std::ostream* out)
-    : SygusEnumeratorCallback(env, e, s),
+    : SygusEnumeratorCallback(env, e, tds, s),
       d_eec(eec),
       d_samplerRrV(ssrv),
       d_out(out)
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.h b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h
index 9b7c3fd98..a83e1b071 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator_callback.h
+++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h
@@ -31,6 +31,7 @@ namespace quantifiers {
 class ExampleEvalCache;
 class SygusStatistics;
 class SygusSampler;
+class TermDbSygus;
 
 /**
  * Base class for callbacks in the fast enumerator. This allows a user to
@@ -40,7 +41,10 @@ class SygusSampler;
 class SygusEnumeratorCallback : protected EnvObj
 {
  public:
-  SygusEnumeratorCallback(Env& env, Node e, SygusStatistics* s = nullptr);
+  SygusEnumeratorCallback(Env& env,
+                          Node e,
+                          TermDbSygus* tds = nullptr,
+                          SygusStatistics* s = nullptr);
   virtual ~SygusEnumeratorCallback() {}
   /**
    * Add term, return true if the term should be considered in the enumeration.
@@ -75,6 +79,8 @@ class SygusEnumeratorCallback : protected EnvObj
   Node d_enum;
   /** The type of enum */
   TypeNode d_tn;
+  /** Term database sygus */
+  TermDbSygus* d_tds;
   /** pointer to the statistics */
   SygusStatistics* d_stats;
 };
@@ -84,6 +90,7 @@ class SygusEnumeratorCallbackDefault : public SygusEnumeratorCallback
  public:
   SygusEnumeratorCallbackDefault(Env& env,
                                  Node e,
+                                 TermDbSygus* tds = nullptr,
                                  SygusStatistics* s = nullptr,
                                  ExampleEvalCache* eec = nullptr,
                                  SygusSampler* ssrv = nullptr,
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 60170ceb4..622aa2a6a 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -739,7 +739,7 @@ SygusTypeInfo& TermDbSygus::getTypeInfo(TypeNode tn)
 Node TermDbSygus::rewriteNode(Node n) const
 {
   Node res;
-  if (options().quantifiers.sygusExtRew)
+  if (options().datatypes.sygusRewriter == options::SygusRewriterMode::EXTENDED)
   {
     res = extendedRewrite(n);
   }
@@ -855,7 +855,8 @@ bool TermDbSygus::canConstructKind(TypeNode tn,
     }
     return true;
   }
-  if (!options().datatypes.sygusSymBreakAgg)
+  if (options().datatypes.sygusSimpleSymBreak
+      != options::SygusSimpleSymBreakMode::AGG)
   {
     return false;
   }
diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp
index bfe9021aa..262459b4f 100644
--- a/src/theory/strings/rewrites.cpp
+++ b/src/theory/strings/rewrites.cpp
@@ -91,6 +91,7 @@ const char* toString(Rewrite r)
     case Rewrite::RE_IN_SIGMA_STAR: return "RE_IN_SIGMA_STAR";
     case Rewrite::RE_IN_CHAR_MODULUS_STAR: return "RE_IN_CHAR_MODULUS_STAR";
     case Rewrite::RE_LOOP: return "RE_LOOP";
+    case Rewrite::RE_LOOP_NONE: return "RE_LOOP_NONE";
     case Rewrite::RE_LOOP_STAR: return "RE_LOOP_STAR";
     case Rewrite::RE_OR_ALL: return "RE_OR_ALL";
     case Rewrite::RE_SIMPLE_CONSUME: return "RE_SIMPLE_CONSUME";
diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h
index b57c5f276..eedd0fb40 100644
--- a/src/theory/strings/rewrites.h
+++ b/src/theory/strings/rewrites.h
@@ -94,6 +94,7 @@ enum class Rewrite : uint32_t
   RE_IN_SIGMA_STAR,
   RE_IN_CHAR_MODULUS_STAR,
   RE_LOOP,
+  RE_LOOP_NONE,
   RE_LOOP_STAR,
   RE_OR_ALL,
   RE_SIMPLE_CONSUME,
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 1094bd14d..374b43c34 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -1166,15 +1166,24 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node)
 Node SequencesRewriter::rewriteLoopRegExp(TNode node)
 {
   Assert(node.getKind() == REGEXP_LOOP);
-  Node retNode = node;
+  uint32_t l = utils::getLoopMinOccurrences(node);
+  uint32_t u = utils::getLoopMaxOccurrences(node);
   Node r = node[0];
-  if (r.getKind() == REGEXP_STAR)
+  Node retNode = node;
+
+  NodeManager* nm = NodeManager::currentNM();
+  if (u < l)
+  {
+    // ((_ re.loop l u) r) --> re.none if u < l
+    std::vector<Node> nvec;
+    retNode = nm->mkNode(REGEXP_NONE, nvec);
+    return returnRewrite(node, retNode, Rewrite::RE_LOOP_NONE);
+  }
+  else if (r.getKind() == REGEXP_STAR)
   {
     return returnRewrite(node, r, Rewrite::RE_LOOP_STAR);
   }
-  NodeManager* nm = NodeManager::currentNM();
-  cvc5::Rational rMaxInt(String::maxSize());
-  uint32_t l = utils::getLoopMinOccurrences(node);
+
   std::vector<Node> vec_nodes;
   for (unsigned i = 0; i < l; i++)
   {
@@ -1184,13 +1193,7 @@ Node SequencesRewriter::rewriteLoopRegExp(TNode node)
       vec_nodes.size() == 0
           ? nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String("")))
           : vec_nodes.size() == 1 ? r : nm->mkNode(REGEXP_CONCAT, vec_nodes);
-  uint32_t u = utils::getLoopMaxOccurrences(node);
-  if (u < l)
-  {
-    std::vector<Node> nvec;
-    retNode = nm->mkNode(REGEXP_NONE, nvec);
-  }
-  else if (u == l)
+  if (u == l)
   {
     retNode = n;
   }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 7c536454a..70331803c 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1293,6 +1293,7 @@ set(regress_0_tests
   regress0/strings/parser-syms.cvc.smt2
   regress0/strings/proj-issue316-regexp-ite.smt2
   regress0/strings/proj-issue390-update-rev-rewrite.smt2
+  regress0/strings/proj-issue409-re-loop-none.smt2
   regress0/strings/re_diff.smt2
   regress0/strings/re-in-rewrite.smt2
   regress0/strings/re-syntax.smt2
diff --git a/test/regress/regress0/strings/proj-issue409-re-loop-none.smt2 b/test/regress/regress0/strings/proj-issue409-re-loop-none.smt2
new file mode 100644
index 000000000..75570864f
--- /dev/null
+++ b/test/regress/regress0/strings/proj-issue409-re-loop-none.smt2
@@ -0,0 +1,4 @@
+(set-logic QF_SLIA)
+(assert (str.in_re (str.from_code 0) ((_ re.loop 2 1) re.all)))
+(set-info :status unsat)
+(check-sat)
diff --git a/test/regress/regress1/rr-verify/bool-crci.sy b/test/regress/regress1/rr-verify/bool-crci.sy
index 75837695d..614a83f2b 100644
--- a/test/regress/regress1/rr-verify/bool-crci.sy
+++ b/test/regress/regress1/rr-verify/bool-crci.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --no-sygus-sym-break
+; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --sygus-simple-sym-break=none
 ; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
 ; EXIT: 1
diff --git a/test/regress/regress1/rr-verify/bv-term-32.sy b/test/regress/regress1/rr-verify/bv-term-32.sy
index 9dfb19451..95296463b 100644
--- a/test/regress/regress1/rr-verify/bv-term-32.sy
+++ b/test/regress/regress1/rr-verify/bv-term-32.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break
+; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --sygus-simple-sym-break=none
 ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
 ; EXIT: 1
diff --git a/test/regress/regress1/rr-verify/bv-term.sy b/test/regress/regress1/rr-verify/bv-term.sy
index 9a11128d7..af954cbb1 100644
--- a/test/regress/regress1/rr-verify/bv-term.sy
+++ b/test/regress/regress1/rr-verify/bv-term.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --no-sygus-sym-break
+; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --sygus-simple-sym-break=none
 ; COMMAND-LINE: --lang=sygus2 --sygus-rr-synth --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --sygus-rr-synth-check
 ; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite|\(rewrite)'
diff --git a/test/regress/regress1/rr-verify/fp-arith.sy b/test/regress/regress1/rr-verify/fp-arith.sy
index 2970fd0de..ad8635ca8 100644
--- a/test/regress/regress1/rr-verify/fp-arith.sy
+++ b/test/regress/regress1/rr-verify/fp-arith.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp
+; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --sygus-simple-sym-break=none --fp-exp
 ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)'
 ; EXIT: 1
diff --git a/test/regress/regress1/rr-verify/fp-bool.sy b/test/regress/regress1/rr-verify/fp-bool.sy
index e4b3a0fac..33caed2e9 100644
--- a/test/regress/regress1/rr-verify/fp-bool.sy
+++ b/test/regress/regress1/rr-verify/fp-bool.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp
+; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --sygus-simple-sym-break=none --fp-exp
 ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)'
 ; EXIT: 1
diff --git a/test/regress/regress1/rr-verify/string-term.sy b/test/regress/regress1/rr-verify/string-term.sy
index 404719f6c..815cb70a5 100644
--- a/test/regress/regress1/rr-verify/string-term.sy
+++ b/test/regress/regress1/rr-verify/string-term.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break
+; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --sygus-simple-sym-break=none
 ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
 ; EXIT: 1
diff --git a/test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2 b/test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2
index a7c864544..cc0c329cd 100644
--- a/test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2
+++ b/test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2
@@ -1,6 +1,6 @@
 (set-logic ALL)
 (set-option :sygus-inference true)
-(set-option :sygus-sym-break false)
+(set-option :sygus-simple-sym-break none)
 (set-option :sygus-sym-break-lazy false)
 (set-option :sygus-sym-break-rlv false)
 (set-info :status sat)