Decouple fmf-bound and finite-model-find (#3297)

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