From 49c2b740513ad4e6a256e1758575bd898afbdfc5 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Sat, 29 May 2010 00:14:09 +0000
Subject: [PATCH] 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.

---
 src/theory/theory_engine.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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);
-- 
2.30.2