Combine sygus stream with PBE (#2726)

1 files changed, 5 insertions, 4 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1de3e3756..a0939f4db 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1938,13 +1938,14 @@ void SmtEngine::setDefaults() {
       // Streaming is incompatible with techniques that focus the search towards
       // finding a single solution. This currently includes the PBE solver and
       // static template inference for invariant synthesis.
-      if (!options::sygusSymBreakPbe.wasSetByUser())
-      {
-        options::sygusSymBreakPbe.set(false);
-      }
       if (!options::sygusUnifPbe.wasSetByUser())
       {
         options::sygusUnifPbe.set(false);
+        // also disable PBE-specific symmetry breaking unless PBE was enabled
+        if (!options::sygusSymBreakPbe.wasSetByUser())
+        {
+          options::sygusSymBreakPbe.set(false);
+        }
       }
       if (!options::sygusInvTemplMode.wasSetByUser())
       {