From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 12 Oct 2010 21:59:40 +0000 (+0000)
Subject: fix debugPrintNode(), debugPrintTNode(), debugPrintNodeValue(), debugPrintTypeNode... 
X-Git-Tag: cvc5-1.0.0~8806
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8a00a28423e3a9d363b98cc5713af3a621b3b7e0;p=cvc5.git

fix debugPrintNode(), debugPrintTNode(), debugPrintNodeValue(), debugPrintTypeNode() -- thanks Tim for pointing this out
---

diff --git a/src/expr/node.h b/src/expr/node.h
index 1427bb9c2..6089eea4d 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -1127,7 +1127,9 @@ Node NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
  * to meet. A cleaner solution is welcomed.
  */
 static void __attribute__((used)) debugPrintNode(const NodeTemplate<true>& n) {
-  Warning() << Node::setdepth(-1) << n << std::endl;
+  Warning() << Node::setdepth(-1)
+            << Node::setlanguage(language::output::LANG_AST)
+            << n << std::endl;
   Warning().flush();
 }
 static void __attribute__((used)) debugPrintRawNode(const NodeTemplate<true>& n) {
@@ -1136,7 +1138,9 @@ static void __attribute__((used)) debugPrintRawNode(const NodeTemplate<true>& n)
 }
 
 static void __attribute__((used)) debugPrintTNode(const NodeTemplate<false>& n) {
-  Warning() << Node::setdepth(-1) << n << std::endl;
+  Warning() << Node::setdepth(-1)
+            << Node::setlanguage(language::output::LANG_AST)
+            << n << std::endl;
   Warning().flush();
 }
 static void __attribute__((used)) debugPrintRawTNode(const NodeTemplate<false>& n) {
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index a42f39e15..1256ec64f 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -471,7 +471,9 @@ inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) {
  * flushes the stream.
  */
 static void __attribute__((used)) debugPrintNodeValue(const expr::NodeValue* nv) {
-  Warning() << Node::setdepth(-1) << *nv << std::endl;
+  Warning() << Node::setdepth(-1)
+            << Node::setlanguage(language::output::LANG_AST)
+            << *nv << std::endl;
   Warning().flush();
 }
 
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index cc368e8c0..27cedf00d 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -567,7 +567,9 @@ inline void TypeNode::printAst(std::ostream& out, int indent) const {
  * to meet. A cleaner solution is welcomed.
  */
 static void __attribute__((used)) debugPrintTypeNode(const TypeNode& n) {
-  Warning() << Node::setdepth(-1) << n << std::endl;
+  Warning() << Node::setdepth(-1)
+            << Node::setlanguage(language::output::LANG_AST)
+            << n << std::endl;
   Warning().flush();
 }
 static void __attribute__((used)) debugPrintRawTypeNode(const TypeNode& n) {