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

2 files changed, 3 insertions, 3 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;
 }
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index dcb37d3d9..ef8c8fcbc 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -102,7 +102,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   }
 
   // constant
-  if(n.isConst()) {
+  if(n.getMetaKind() == kind::metakind::CONSTANT) {
     switch(n.getKind()) {
     case kind::TYPE_CONSTANT:
       switch(n.getConst<TypeConstant>()) {