diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 116d2fe23..15b6e2fc9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1403,6 +1403,8 @@ void SmtEngine::setDefaults() { d_logic = d_logic.getUnlockedCopy(); d_logic.enableTheory(THEORY_DATATYPES); d_logic.lock(); + // since we are trying to recast as sygus, we assume the input is sygus + is_sygus = true; } if ((options::checkModels() || options::checkSynthSol()) @@ -2053,6 +2055,10 @@ void SmtEngine::setDefaults() { if( !options::miniscopeQuantFreeVar.wasSetByUser() ){ options::miniscopeQuantFreeVar.set( false ); } + if (!options::quantSplit.wasSetByUser()) + { + options::quantSplit.set(false); + } //rewrite divk if( !options::rewriteDivk.wasSetByUser()) { options::rewriteDivk.set( true ); |