diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-10-30 15:27:10 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-10-30 15:27:10 -0700 |
commit | 43ab3f4cd1aa5549cb1aa3c20a2d589614bcb8fc (patch) | |
tree | cf7b5d7f73a4d4ddc34492334a7d0eb90b57b77b /src/theory/rewriter.cpp | |
parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'src/theory/rewriter.cpp')
-rw-r--r-- | src/theory/rewriter.cpp | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 045ac3f39..866883681 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -222,15 +222,18 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { } else if (response.status == REWRITE_DONE) { #ifdef CVC4_ASSERTIONS RewriteResponse r2 = Rewriter::callPostRewrite(newTheoryId, response.node); - Assert(r2.node == response.node); + Assert(r2.node == response.node); #endif rewriteStackTop.node = response.node; break; } // 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; + 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 Rewriter::setPostRewriteCache((TheoryId) rewriteStackTop.originalTheoryId, rewriteStackTop.original, rewriteStackTop.node); @@ -243,7 +246,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { // If this is the last node, just return if (rewriteStack.size() == 1) { - Assert(!isEquality || rewriteStackTop.node.getKind() == kind::EQUAL || rewriteStackTop.node.isConst()); + Assert(!isEquality || rewriteStackTop.node.getKind() == kind::EQUAL + || rewriteStackTop.node.isConst()); return rewriteStackTop.node; } |