1 files changed, 5 insertions, 12 deletions
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index f8d62a8be..5d54759b9 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Aina Niemetz, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -52,14 +52,6 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang)
   case LANG_CVC4:
     return unique_ptr<Printer>(new printer::cvc::CvcPrinter());
 
-  case LANG_Z3STR:
-    return unique_ptr<Printer>(
-        new printer::smt2::Smt2Printer(printer::smt2::z3str_variant));
-
-  case LANG_SYGUS_V1:
-    return unique_ptr<Printer>(
-        new printer::smt2::Smt2Printer(printer::smt2::sygus_variant));
-
   case LANG_SYGUS_V2:
     // sygus version 2.0 does not have discrepancies with smt2, hence we use
     // a normal smt2 variant here.
@@ -122,9 +114,10 @@ Printer* Printer::getPrinter(OutputLanguage lang)
       lang = language::toOutputLanguage(options::inputLanguage());
      }
    }
-   if(lang == language::output::LANG_AUTO) {
-      lang = language::output::LANG_CVC4; // default
-    }
+   if (lang == language::output::LANG_AUTO)
+   {
+     lang = language::output::LANG_SMTLIB_V2_6;  // default
+   }
   }
   if(d_printers[lang] == NULL) {
     d_printers[lang] = makePrinter(lang);