Reduce before preregister. (#2025)

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 944010ab13d42ca489a30cc2efeb6fa7b481ab3e..f8053f2b360c33eff88ec382e99af94a09683b49 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -788,6 +788,12 @@ void QuantifiersEngine::preRegisterQuantifier(Node q)
   }
   Trace("quant-debug") << "QuantifiersEngine : Pre-register " << q << std::endl;
   d_quants_prereg.insert(q);
+  // try to reduce
+  if (reduceQuantifier(q))
+  {
+    // if we can reduce it, nothing left to do
+    return;
+  }
   // ensure that it is registered
   registerQuantifierInternal(q);
   // register with each module