diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-02 20:08:53 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-07-02 20:08:53 -0500 |
| commit | 0dec323ac1b45ce1ca194e9bb2a335c8def525d2 (patch) | |
| tree | c201933c725ddfd7f68a1e03db8e4f85242d0d6c /src/smt | |
| parent | be58c8ead1d36ab3625faf848b2ebdce8d5de8a9 (diff) | |
Remove miscellaneous dead and unused code from quantifiers (#2121)
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1705cd0a3..53ea9fd58 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1916,10 +1916,10 @@ void SmtEngine::setDefaults() { if( options::fmfBound() ){ //must have finite model finding on options::finiteModelFind.set( true ); - if( ! options::mbqiMode.wasSetByUser() || - ( options::mbqiMode()!=quantifiers::MBQI_NONE && - options::mbqiMode()!=quantifiers::MBQI_FMC && - options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL ) ){ + if (!options::mbqiMode.wasSetByUser() + || (options::mbqiMode() != quantifiers::MBQI_NONE + && options::mbqiMode() != quantifiers::MBQI_FMC)) + { //if bounded integers are set, use no MBQI by default options::mbqiMode.set( quantifiers::MBQI_NONE ); } |