From 4be329c881c510caab5995b5ecbe3ae9961b3eed Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 31 May 2018 19:06:55 -0500
Subject: [PATCH] Reduce before preregister. (#2025)

---
 src/theory/quantifiers_engine.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 944010ab1..f8053f2b3 100644
--- 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
-- 
2.30.2