minor isConst()-related fixes to printing; also add some debugging stuff to see how isConst() operates: use -d isConst

1 files changed, 2 insertions, 2 deletions

diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp
index 580bec63c..f22b35152 100644
--- a/src/printer/dagification_visitor.cpp
+++ b/src/printer/dagification_visitor.cpp
@@ -54,11 +54,11 @@ bool DagificationVisitor::alreadyVisited(TNode current, TNode parent) {
   // for all subexpressions, so it isn't useful to traverse and
   // increment again (they'll be dagified anyway).
   return current.isVar() ||
-         current.isConst() ||
+         current.getMetaKind() == kind::metakind::CONSTANT ||
          ( ( current.getKind() == kind::NOT ||
              current.getKind() == kind::UMINUS ) &&
            ( current[0].isVar() ||
-             current[0].isConst() ) ) ||
+             current[0].getMetaKind() == kind::metakind::CONSTANT ) ) ||
          current.getKind() == kind::SORT_TYPE ||
          d_nodeCount[current] > d_threshold;
 }