diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-20 09:02:25 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-20 09:02:25 -0500 |
commit | 9d9a8bbd4465efd0860b185889fae89e4693d2a2 (patch) | |
tree | ec42e3da1ce7d790ece4e1e1df6e35f65c782041 /src/smt/smt_engine.cpp | |
parent | f25f227eb4a4df388160cdf62795f7f684b224ea (diff) | |
parent | 1d4324bf87a35e36d9cc1e856d74ffbaf912a848 (diff) |
Merge branch 'master' into strRewritesstrRewrites
Diffstat (limited to 'src/smt/smt_engine.cpp')
-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() ){ |