diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-17 14:22:26 -0600 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-17 14:23:03 -0600 |
commit | 856cc3f45a1b2da648a6b85a5e774c260a83c596 (patch) | |
tree | 537ecf06470dc2087a99793189c130f4d4d81256 /src/smt | |
parent | eb5debabce433774a0dbfd46745efb8fcf38b8ab (diff) |
type conversion
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 ef4f01cd1..dcca1624d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -954,10 +954,16 @@ void SmtEngine::setLogicInternal() throw() { 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 ); Trace("smt") << "turning on strings-fmf, for strings-exp" << std::endl; - } + }*/ } // by default, symmetry breaker is on only for QF_UF |