diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3a138e4b7..54deba78c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1343,6 +1343,10 @@ void SmtEngine::setDefaults() { options::fmfBoundInt.set( true ); Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl; } + if(! options::fmfInstEngine.wasSetByUser()) { + options::fmfInstEngine.set( true ); + Trace("smt") << "turning on fmf-inst-engine, for strings-exp" << std::endl; + } /* if(! options::rewriteDivk.wasSetByUser()) { options::rewriteDivk.set( true ); @@ -3895,7 +3899,6 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertions : " << d_assertions.size() << endl; - dumpAssertions("pre-constrain-subtypes", d_assertions); { // Any variables of subtype types need to be constrained properly. |