* Rename SMT parts (printer, parser) to SMT1

* Change --lang smt to mean SMT-LIBv2
* --lang smt1 now means SMT-LIBv1

* SMT-LIBv2 parser now gives helpful error if input looks like v1
* SMT-LIBv1 parser now gives helpful error if input looks like v2
* CVC presentation language parser now gives helpful error if input
  looks like either SMT-LIB v1 or v2

* Other associated changes

(this commit was certified error- and warning-free by the test-and-commit script.)

1 files changed, 3 insertions, 3 deletions

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 222a22e34..f20ab2901 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -20,7 +20,7 @@
 
 #include "util/language.h"
 
-#include "printer/smt/smt_printer.h"
+#include "printer/smt1/smt1_printer.h"
 #include "printer/smt2/smt2_printer.h"
 #include "printer/cvc/cvc_printer.h"
 #include "printer/ast/ast_printer.h"
@@ -37,8 +37,8 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() {
   using namespace CVC4::language::output;
 
   switch(lang) {
-  case LANG_SMTLIB:
-    return new printer::smt::SmtPrinter();
+  case LANG_SMTLIB_V1:
+    return new printer::smt1::Smt1Printer();
 
   case LANG_SMTLIB_V2:
     return new printer::smt2::Smt2Printer();