diff options
Diffstat (limited to 'src/theory/rewriter.cpp')
| -rw-r--r-- | src/theory/rewriter.cpp | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 18ded60a8..b99c14a24 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -17,10 +17,10 @@ #include "theory/rewriter.h" -#include "theory/theory.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "theory/rewriter_tables.h" +#include "theory/theory.h" #include "util/resource_manager.h" using namespace std; @@ -159,7 +159,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { } } - rewriteStackTop.original =rewriteStackTop.node; + rewriteStackTop.original = rewriteStackTop.node; // Now it's time to rewrite the children, check if this has already been done Node cached = Rewriter::getPostRewriteCache((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node); // If not, go through the children @@ -219,16 +219,16 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { break; } else if (response.status == REWRITE_DONE) { #ifdef CVC4_ASSERTIONS - RewriteResponse r2 = Rewriter::callPostRewrite(newTheoryId, response.node); - Assert(r2.node == response.node); + RewriteResponse r2 = Rewriter::callPostRewrite(newTheoryId, response.node); + Assert(r2.node == response.node); #endif - rewriteStackTop.node = response.node; + 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; + 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); |