1 files changed, 3 insertions, 0 deletions
diff --git a/src/printer/printer.h b/src/printer/printer.h
index d3a9201ee..6fe1ec279 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -53,6 +53,9 @@ protected:
 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
+    }
     if(d_printers[lang] == NULL) {
       d_printers[lang] = makePrinter(lang);
     }