From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 1 Jun 2018 00:06:55 +0000 (-0500)
Subject: Reduce before preregister. (#2025)
X-Git-Tag: cvc5-1.0.0~4990
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4be329c881c510caab5995b5ecbe3ae9961b3eed;p=cvc5.git

Reduce before preregister. (#2025)
---

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