diff options
Diffstat (limited to 'src/theory/rewriter.cpp')
-rw-r--r-- | src/theory/rewriter.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 7d5f541c0..0c5cada09 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -163,6 +163,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { TheoryId newTheoryId = Theory::theoryOf(response.node); if (newTheoryId != (TheoryId) rewriteStackTop.theoryId || response.status == REWRITE_AGAIN_FULL) { // In the post rewrite if we've changed theories, we must do a full rewrite + Assert(response.node != rewriteStackTop.node); rewriteStackTop.node = rewriteTo(newTheoryId, response.node); break; } else if (response.status == REWRITE_DONE) { @@ -173,7 +174,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { rewriteStackTop.node = response.node; break; } - // Check for trivial rewrite loop of size 2 + // Check for trivial rewrite loops of size 1 or 2 + Assert(response.node != rewriteStackTop.node); Assert(Rewriter::callPostRewrite((TheoryId) rewriteStackTop.theoryId, response.node).node != rewriteStackTop.node); rewriteStackTop.node = response.node; } |