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.

1 files changed, 1 insertions, 1 deletions

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