diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-08-17 11:53:11 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-08-17 11:53:11 +0200 |
| commit | 7766f0ba088ad6d6c58ea9678477b255c9e52fee (patch) | |
| tree | e8f1374804ab2df1f67c48793993eb65d68a6496 /src/theory/quantifiers_engine.cpp | |
| parent | 6432a16bd86c7540dad4ce5321ee68b7a7287c66 (diff) | |
Add mbqi interleave option, change option fs-inst to fs-interleave.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index fa1394f39..fd831001f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -265,7 +265,7 @@ void QuantifiersEngine::finishInit(){ d_modules.push_back( d_uee ); } //full saturation : instantiate from relevant domain, then arbitrary terms - if( options::fullSaturateQuant() || options::fullSaturateInst() ){ + if( options::fullSaturateQuant() || options::fullSaturateInterleave() ){ d_fs = new quantifiers::FullSaturation( this ); d_modules.push_back( d_fs ); needsRelDom = true; |