From: Tim King <taking@cs.nyu.edu>
Date: Sat, 29 May 2010 00:14:09 +0000 (+0000)
Subject: After blasting the disjuncts, TheoryEngine rewrite needs to reinvoke itself. QF_LRA... 
X-Git-Tag: cvc5-1.0.0~9022
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=49c2b740513ad4e6a256e1758575bd898afbdfc5;p=cvc5.git

After blasting the disjuncts, TheoryEngine rewrite needs to reinvoke itself. QF_LRA is now no longer complaining about seeing nodes that can be rewritten to CONST_BOOLEAN.
---

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index c89e767f4..476091723 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -176,7 +176,7 @@ Node TheoryEngine::rewrite(TNode in) {
   if(intermediate.getKind() == kind::DISTINCT) {
     Node out = blastDistinct(intermediate);
     //setRewriteCache(intermediate, out);
-    return out;
+    return rewrite(out); //TODO let this fall through?
   }
 
   theory::Theory* thy = theoryOf(intermediate);