diff options
author | Tim King <taking@cs.nyu.edu> | 2010-05-29 00:14:09 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-05-29 00:14:09 +0000 |
commit | 49c2b740513ad4e6a256e1758575bd898afbdfc5 (patch) | |
tree | 2f857f4d546499e2b488477a38cb35e38930e270 | |
parent | c5f652834b915641ae6cbeccf97e959470757863 (diff) |
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.
-rw-r--r-- | src/theory/theory_engine.cpp | 2 |
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); |