diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-01-22 13:40:54 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-01-22 13:40:54 -0600 |
| commit | fffb74dbd0ee96b636fb494e843dd760b1a13149 (patch) | |
| tree | 693cfca9982ce0257fd132e956b32f7f681954db /src/smt | |
| parent | 3da57075e8f810773ae95aadadc5408e0a537f02 (diff) | |
add warning for using strings in ALL_SUPPORTED
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4e0ea51a6..46843b21a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -950,20 +950,14 @@ void SmtEngine::setLogicInternal() throw() { d_logic.enableQuantifiers(); d_logic.lock(); Trace("smt") << "turning on quantifier logic, for strings-exp" << std::endl; - //exception - //throw OptionException("The string-exp option requires quantifier option. One suggestion is UFSLIA."); } if(! options::finiteModelFind.wasSetByUser()) { - //exception - throw OptionException("The string-exp option requires finite-model-find option."); - //options::finiteModelFind.set( true ); - //Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl; + options::finiteModelFind.set( true ); + Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl; } if(! options::fmfBoundInt.wasSetByUser()) { - //exception - throw OptionException("The string-exp option requires fmf-bound-int option."); - //options::fmfBoundInt.set( true ); - //Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl; + options::fmfBoundInt.set( true ); + Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl; } if(! options::stringFMF.wasSetByUser()) { options::stringFMF.set( true ); |