Disable sygus PBE when sygus stream is enabled (#1451)

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index c3091a131ebd5190826025ee0df24dadc34a17d2..65731547dd7f46666d9629f69b893a10814c75e2 100644 (file)
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -261,7 +261,7 @@ option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default
   include constants when reconstruct solutions for single invocation conjectures in original grammar
 option cegqiSingleInvAbort --cegqi-si-abort bool :default false
   abort if synthesis conjecture is not single invocation
-option sygusPbe --sygus-pbe bool :default true
+option sygusPbe --sygus-pbe bool :default true :read-write
   sygus advanced pruning based on examples
 option sygusQePreproc --sygus-qe-preproc bool :default false
   use quantifier elimination as a preprocessing step for sygus

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4336b7a0503a20ceecfb2a7fb8eded8f52c1d7cf..9b4837d439c3bc662336799446215f2d760fdcc2 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1873,6 +1873,14 @@ void SmtEngine::setDefaults() {
     if( !options::instNoEntail.wasSetByUser() ){
       options::instNoEntail.set( false );
     }
+    if (options::sygusStream())
+    {
+      // PBE and streaming modes are incompatible
+      if (!options::sygusPbe.wasSetByUser())
+      {
+        options::sygusPbe.set(false);
+      }
+    }
     //do not allow partial functions
     if( !options::bitvectorDivByZeroConst.wasSetByUser() ){
       options::bitvectorDivByZeroConst.set( true );