diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-18 15:03:12 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-18 15:03:12 -0500 |
commit | a9c40f60e4b36494e10520dcc3a3985b4700342f (patch) | |
tree | 70dc9c73b5ce2007850ab40e623a55d205ba62e4 /src/theory | |
parent | 40b83fd9205a7eb772a2ac413f8a3641db1fb02c (diff) |
Decouple fmf-bound and finite-model-find (#3297)
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 |