Merge branch '1.3.x'

Conflicts:
	NEWS

2 files changed, 16 insertions, 2 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 49ded4ecb..ca463d10b 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -80,7 +80,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
 
   // null
   if(n.getKind() == kind::NULL_EXPR) {
-    out << "NULL";
+    out << "null";
     return;
   }
 
diff --git a/src/printer/printer.h b/src/printer/printer.h
index a7ae8c447..9ddac096d 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -54,7 +54,21 @@ public:
   /** Get the Printer for a given OutputLanguage */
   static Printer* getPrinter(OutputLanguage lang) throw() {
     if(lang == language::output::LANG_AUTO) {
-      lang = language::output::LANG_CVC4; // default
+      // Infer the language to use for output.
+      //
+      // Options can be null in certain circumstances (e.g., when printing
+      // the singleton "null" expr.  So we guard against segfault
+      if(&Options::current() != NULL) {
+        if(options::outputLanguage.wasSetByUser()) {
+          lang = options::outputLanguage();
+        }
+        if(lang == language::output::LANG_AUTO && options::inputLanguage.wasSetByUser()) {
+          lang = language::toOutputLanguage(options::inputLanguage());
+        }
+      }
+      if(lang == language::output::LANG_AUTO) {
+        lang = language::output::LANG_CVC4; // default
+      }
     }
     if(d_printers[lang] == NULL) {
       d_printers[lang] = makePrinter(lang);