diff options
Diffstat (limited to 'src/theory/strings/sequences_rewriter.h')
-rw-r--r-- | src/theory/strings/sequences_rewriter.h | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h index 5aba4ab6f..a98ad97ac 100644 --- a/src/theory/strings/sequences_rewriter.h +++ b/src/theory/strings/sequences_rewriter.h @@ -23,6 +23,7 @@ #include <vector> #include "expr/attribute.h" +#include "theory/strings/rewrites.h" #include "theory/theory_rewriter.h" #include "theory/type_enumerator.h" @@ -149,7 +150,7 @@ class SequencesRewriter : public TheoryRewriter /** * Called when node rewrites to ret. * - * The string c indicates the justification for the rewrite, which is printed + * The rewrite r indicates the justification for the rewrite, which is printed * by this function for debugging. * * If node is not an equality and ret is an equality, this method applies @@ -157,7 +158,7 @@ class SequencesRewriter : public TheoryRewriter * additional rewrites on ret, after which we return the result of this call. * Otherwise, this method simply returns ret. */ - static Node returnRewrite(Node node, Node ret, const char* c); + static Node returnRewrite(Node node, Node ret, Rewrite r); public: RewriteResponse postRewrite(TNode node) override; |