diff options
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e5db42a22..149d8bb35 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1927,7 +1927,9 @@ void SmtEngine::setDefaults() { } if (options::sygusStream()) { - // PBE and streaming modes are incompatible + // 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); @@ -1936,6 +1938,10 @@ void SmtEngine::setDefaults() { { options::sygusUnifPbe.set(false); } + if (!options::sygusInvTemplMode.wasSetByUser()) + { + options::sygusInvTemplMode.set(quantifiers::SYGUS_INV_TEMPL_MODE_NONE); + } } //do not allow partial functions if( !options::bitvectorDivByZeroConst.wasSetByUser() ){ |