diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 1eb62945b..e399af71d 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -138,13 +138,13 @@ class QuantifiersEnginePrivate modules.push_back(d_synth_e.get()); } // finite model finding - if (options::finiteModelFind()) + if (options::fmfBound()) + { + d_bint.reset(new quantifiers::BoundedIntegers(c, qe)); + modules.push_back(d_bint.get()); + } + if (options::finiteModelFind() || options::fmfBound()) { - if (options::fmfBound()) - { - d_bint.reset(new quantifiers::BoundedIntegers(c, qe)); - modules.push_back(d_bint.get()); - } d_model_engine.reset(new quantifiers::ModelEngine(c, qe)); modules.push_back(d_model_engine.get()); // finite model finder has special ways of building the model |