From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 29 Oct 2011 08:11:12 +0000 (+0000)
Subject: fix unit tests
X-Git-Tag: cvc5-1.0.0~8402
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cfcb83489f040f753a7da1a66bb548728f239a61;p=cvc5.git

fix unit tests
---

diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index f1fade69d..89ac7ffca 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -39,7 +39,11 @@ NodeValue NodeValue::s_null(0);
 
 string NodeValue::toString() const {
   stringstream ss;
-  toStream(ss, -1, false, Options::current()->outputLanguage);
+  OutputLanguage outputLanguage = (this == &s_null) ? language::output::LANG_AST : Options::current()->outputLanguage;
+  toStream(ss, -1, false,
+           outputLanguage == language::output::LANG_AUTO ?
+             language::output::LANG_AST :
+             outputLanguage);
   return ss.str();
 }