diff options
Diffstat (limited to 'src/theory/rewriter.cpp')
| -rw-r--r-- | src/theory/rewriter.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 18274e060..7d5f541c0 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -173,6 +173,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { rewriteStackTop.node = response.node; break; } + // Check for trivial rewrite loop of size 2 + Assert(Rewriter::callPostRewrite((TheoryId) rewriteStackTop.theoryId, response.node).node != rewriteStackTop.node); rewriteStackTop.node = response.node; } // We're done with the post rewrite, so we add to the cache |