After blasting the disjuncts, TheoryEngine rewrite needs to reinvoke itself. QF_LRA...

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index c89e767f47600afe0d478770c865f7f6b395c2ff..476091723bc17f18f45d8e905e3e6f361ceb57bb 100644 (file)
--- 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);