diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 9abd6e165..4719af3c0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -793,6 +793,14 @@ void SmtEngine::finalOptionsAreSet() { return; } + // set strings-exp + /* + if(!d_logic.hasEverything() && d_logic.isTheoryEnabled(THEORY_STRINGS) ) { + if(! options::stringExp.wasSetByUser()) { + options::stringExp.set( true ); + Trace("smt") << "turning on strings-exp, for the theory of strings" << std::endl; + } + }*/ // for strings if(options::stringExp()) { if( !d_logic.isQuantified() ) { @@ -808,11 +816,11 @@ void SmtEngine::finalOptionsAreSet() { options::fmfBoundInt.set( true ); Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl; } + /* if(! options::rewriteDivk.wasSetByUser()) { options::rewriteDivk.set( true ); Trace("smt") << "turning on rewrite-divk, for strings-exp" << std::endl; - } - + }*/ /* if(! options::stringFMF.wasSetByUser()) { options::stringFMF.set( true ); |