summaryrefslogtreecommitdiff
path: root/src/theory/bv/theory_bv_rewriter.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv/theory_bv_rewriter.h')
-rw-r--r--src/theory/bv/theory_bv_rewriter.h4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index 20da74ce8..11a55ca61 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -42,6 +42,10 @@ public:
return RewriteResponse(REWRITE_DONE, node);
}
+ static inline Node rewriteEquality(TNode node) {
+ return postRewrite(node).node;
+ }
+
static void init();
static void shutdown();
};/* class TheoryBVRewriter */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback