summaryrefslogtreecommitdiff
path: root/src/theory/builtin
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2018-08-16 16:46:05 -0700
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-08-16 18:46:05 -0500
commit7fc04bf78c6c20f3711d14425469eef2e0c2cd60 (patch)
treed9f2e91a52406edf66967faccad550631cd9e4a5 /src/theory/builtin
parent4e62cdade61514f268b96e78e2f82ad12dfcad07 (diff)
Move node algorithms to separate file (#2311)
Diffstat (limited to 'src/theory/builtin')
-rw-r--r--src/theory/builtin/theory_builtin_rewriter.cpp3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index da28b1ffd..4c14ec177 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -19,6 +19,7 @@
#include "theory/builtin/theory_builtin_rewriter.h"
#include "expr/chain.h"
+#include "expr/node_algorithm.h"
using namespace std;
@@ -88,7 +89,7 @@ RewriteResponse TheoryBuiltinRewriter::postRewrite(TNode node) {
Trace("builtin-rewrite") << " array rep : " << anode << ", constant = " << anode.isConst() << std::endl;
Assert( anode.isConst()==retNode.isConst() );
Assert( retNode.getType()==node.getType() );
- Assert(node.hasFreeVar() == retNode.hasFreeVar());
+ Assert(expr::hasFreeVar(node) == expr::hasFreeVar(retNode));
return RewriteResponse(REWRITE_DONE, retNode);
}
}else{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback