diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-28 16:26:57 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-28 16:26:57 -0500 |
commit | f582b382a25463cead88bc1a46b93dd5c8099fad (patch) | |
tree | 15c54d5b5dc5b9b8a4da72a81c9ed0cf2ee6dc3d /src/smt/smt_engine.cpp | |
parent | 358e453bda62923fd0be94af5317b24a7281014b (diff) |
Minor cleanup from last commit (quant util, equality infer). Do not set fmfBoundIntLazy for stringsExp.
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index bbaa07af5..98ed9c4fd 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1310,15 +1310,7 @@ void SmtEngine::setDefaults() { Trace("smt") << "turning on quantifier logic, for strings-exp" << std::endl; } - if(! options::finiteModelFind.wasSetByUser()) { - options::finiteModelFind.set( true ); - Trace("smt") << "turning on finite-model-find, for strings-exp" - << std::endl; - } if(! options::fmfBoundInt.wasSetByUser()) { - if(! options::fmfBoundIntLazy.wasSetByUser()) { - options::fmfBoundIntLazy.set( true ); - } options::fmfBoundInt.set( true ); Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl; } |