* 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.)

17 files changed, 159 insertions, 135 deletions

diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 01b4e359f..6ef353752 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -17,7 +17,7 @@ AM_CPPFLAGS = \
 	-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. $(ANTLR_INCLUDES)
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
-SUBDIRS = smt smt2 cvc tptp
+SUBDIRS = smt1 smt2 cvc tptp
 
 lib_LTLIBRARIES = libcvc4parser.la
 if HAVE_CXXTESTGEN
@@ -29,14 +29,14 @@ libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS) \
 libcvc4parser_noinst_la_LDFLAGS = $(ANTLR_LDFLAGS)
 
 libcvc4parser_la_LIBADD = \
-	@builddir@/smt/libparsersmt.la \
+	@builddir@/smt1/libparsersmt1.la \
 	@builddir@/smt2/libparsersmt2.la \
 	@builddir@/tptp/libparsertptp.la \
 	@builddir@/cvc/libparsercvc.la \
 	@builddir@/../lib/libreplacements.la \
 	-L@builddir@/.. -lcvc4
 libcvc4parser_noinst_la_LIBADD = \
-	@builddir@/smt/libparsersmt.la \
+	@builddir@/smt1/libparsersmt1.la \
 	@builddir@/smt2/libparsersmt2.la \
 	@builddir@/tptp/libparsertptp.la \
 	@builddir@/cvc/libparsercvc.la \
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 5389f270f..ea593e7da 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -32,7 +32,7 @@
 #include "expr/command.h"
 #include "expr/type.h"
 #include "parser/cvc/cvc_input.h"
-#include "parser/smt/smt_input.h"
+#include "parser/smt1/smt1_input.h"
 #include "parser/smt2/smt2_input.h"
 #include "parser/tptp/tptp_input.h"
 #include "util/output.h"
@@ -194,8 +194,8 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre
     input = new CvcInput(inputStream);
     break;
   }
-  case LANG_SMTLIB:
-    input = new SmtInput(inputStream);
+  case LANG_SMTLIB_V1:
+    input = new Smt1Input(inputStream);
     break;
 
   case LANG_SMTLIB_V2:
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 82e27401e..4577b504c 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -561,6 +561,16 @@ parseExpr returns [CVC4::Expr expr = CVC4::Expr()]
  */
 parseCommand returns [CVC4::Command* cmd = NULL]
   : c=command { $cmd = c; }
+  | LPAREN IDENTIFIER
+    { std::string s = AntlrInput::tokenText($IDENTIFIER);
+      if(s == "benchmark") {
+        PARSER_STATE->parseError("In CVC4 presentation language mode, but SMT-LIBv1 format detected.  Use --lang smt1 for SMT-LIBv1 support.");
+      } else if(s == "set" || s == "get") {
+        PARSER_STATE->parseError("In CVC4 presentation language mode, but SMT-LIBv2 format detected.  Use --lang smt2 for SMT-LIBv2 support.");
+      } else {
+        PARSER_STATE->parseError("A CVC4 presentation language command cannot begin with a parenthesis; expected command name.");
+      }
+    }
   | EOF { $cmd = NULL; }
   ;
 
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index bf7c372b7..2a64d122d 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -31,8 +31,6 @@
 #include "util/output.h"
 #include "options/options.h"
 #include "util/Assert.h"
-#include "parser/cvc/cvc_input.h"
-#include "parser/smt/smt_input.h"
 
 using namespace std;
 using namespace CVC4::kind;
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index bd71f71e7..73c31f578 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -21,7 +21,7 @@
 #include "parser/parser_builder.h"
 #include "parser/input.h"
 #include "parser/parser.h"
-#include "smt/smt.h"
+#include "smt1/smt1.h"
 #include "smt2/smt2.h"
 #include "tptp/tptp.h"
 
@@ -86,8 +86,8 @@ Parser* ParserBuilder::build()
 
   Parser* parser = NULL;
   switch(d_lang) {
-  case language::input::LANG_SMTLIB:
-    parser = new Smt(d_exprManager, input, d_strictMode, d_parseOnly);
+  case language::input::LANG_SMTLIB_V1:
+    parser = new Smt1(d_exprManager, input, d_strictMode, d_parseOnly);
     break;
   case language::input::LANG_SMTLIB_V2:
     parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly);
diff --git a/src/parser/smt/Makefile b/src/parser/smt1/Makefile
index 7e97ed357..7e97ed357 100644
--- a/src/parser/smt/Makefile
+++ b/src/parser/smt1/Makefile
diff --git a/src/parser/smt/Makefile.am b/src/parser/smt1/Makefile.am
index ffc5397c7..34b979ef9 100644
--- a/src/parser/smt/Makefile.am
+++ b/src/parser/smt1/Makefile.am
@@ -12,35 +12,35 @@ ANTLR_OPTS =
 # hide this included makefile from automake
 @mk_include@ @srcdir@/../Makefile.antlr_tracing
 
-noinst_LTLIBRARIES = libparsersmt.la
+noinst_LTLIBRARIES = libparsersmt1.la
 
 ANTLR_TOKEN_STUFF = \
-	generated/Smt.tokens
+	generated/Smt1.tokens
 ANTLR_LEXER_STUFF = \
-	generated/SmtLexer.h \
-	generated/SmtLexer.c \
+	generated/Smt1Lexer.h \
+	generated/Smt1Lexer.c \
 	$(ANTLR_TOKEN_STUFF)
 ANTLR_PARSER_STUFF = \
-	generated/SmtParser.h \
-	generated/SmtParser.c
+	generated/Smt1Parser.h \
+	generated/Smt1Parser.c
 ANTLR_STUFF = \
 	$(ANTLR_LEXER_STUFF) \
 	$(ANTLR_PARSER_STUFF)
 
-libparsersmt_la_SOURCES = \
-	Smt.g \
-        smt.h \
-        smt.cpp \
-	smt_input.h \
-	smt_input.cpp \
+libparsersmt1_la_SOURCES = \
+	Smt1.g \
+        smt1.h \
+        smt1.cpp \
+	smt1_input.h \
+	smt1_input.cpp \
 	$(ANTLR_STUFF)
 
 BUILT_SOURCES = \
-	generated/Smt.tokens \
-	generated/SmtLexer.h \
-	generated/SmtLexer.c \
-	generated/SmtParser.h \
-	generated/SmtParser.c \
+	generated/Smt1.tokens \
+	generated/Smt1Lexer.h \
+	generated/Smt1Lexer.c \
+	generated/Smt1Parser.h \
+	generated/Smt1Parser.c \
 	stamp-generated
 
 DISTCLEANFILES = $(ANTLR_STUFF)
@@ -53,13 +53,13 @@ stamp-generated:
 	$(AM_V_at)touch stamp-generated
 
 # antlr doesn't overwrite output files, it just leaves them.  So we have to delete them first.
-generated/SmtLexer.h: Smt.g stamp-generated
+generated/Smt1Lexer.h: Smt1.g stamp-generated
 	-$(AM_V_at)rm -f $(ANTLR_STUFF)
 	@if test -z "$(ANTLR)"; then echo "ERROR: antlr parser generator cannot be found, cannot generate the parser" >&2; exit 1; fi
-	$(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "generated" "@srcdir@/Smt.g"
+	$(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "generated" "@srcdir@/Smt1.g"
 
-# These don't actually depend on SmtLexer.h, but if we're doing parallel
+# These don't actually depend on Smt1Lexer.h, but if we're doing parallel
 # make and the lexer needs to be rebuilt, we have to keep the rules
 # from running in parallel (since the token files will be deleted &
 # recreated)
-generated/SmtLexer.c generated/SmtParser.h generated/SmtParser.c $(ANTLR_TOKEN_STUFF): generated/SmtLexer.h
+generated/Smt1Lexer.c generated/Smt1Parser.h generated/Smt1Parser.c $(ANTLR_TOKEN_STUFF): generated/Smt1Lexer.h
diff --git a/src/parser/smt/Smt.g b/src/parser/smt1/Smt1.g
index 0298497e9..b228fb9ec 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt1/Smt1.g
@@ -1,5 +1,5 @@
 /* *******************                                                        */
-/*! \file Smt.g
+/*! \file Smt1.g
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: dejan, mdeters
@@ -16,7 +16,7 @@
  ** Parser for SMT-LIB input language.
  **/
 
-grammar Smt;
+grammar Smt1;
 
 options {
   // C output for antlr
@@ -27,7 +27,7 @@ options {
 
   // Only lookahead of <= k requested (disable for LL* parsing)
   // Note that CVC4's BoundedTokenBuffer requires a fixed k !
-  // If you change this k, change it also in smt_input.cpp !
+  // If you change this k, change it also in smt1_input.cpp !
   k = 2;
 }/* options */
 
@@ -75,7 +75,7 @@ namespace CVC4 {
   class Expr;
 
   namespace parser {
-    namespace smt {
+    namespace smt1 {
       /**
        * Just exists to provide the uintptr_t constructor that ANTLR
        * requires.
@@ -97,7 +97,7 @@ namespace CVC4 {
         myType(const Type& t) : CVC4::Type(t) {}
         myType(const myType& t) : CVC4::Type(t) {}
       };/* struct myType */
-    }/* CVC4::parser::smt namespace */
+    }/* CVC4::parser::smt1 namespace */
   }/* CVC4::parser namespace */
 }/* CVC4 namespace */
 
@@ -110,7 +110,7 @@ namespace CVC4 {
 #include "expr/type.h"
 #include "parser/antlr_input.h"
 #include "parser/parser.h"
-#include "parser/smt/smt.h"
+#include "parser/smt1/smt1.h"
 #include "util/integer.h"
 #include "util/output.h"
 #include "util/rational.h"
@@ -122,7 +122,7 @@ using namespace CVC4::parser;
 /* These need to be macros so they can refer to the PARSER macro, which will be defined
  * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
 #undef PARSER_STATE
-#define PARSER_STATE ((Smt*)PARSER->super)
+#define PARSER_STATE ((Smt1*)PARSER->super)
 #undef EXPR_MANAGER
 #define EXPR_MANAGER PARSER_STATE->getExprManager()
 #undef MK_EXPR
@@ -137,7 +137,7 @@ using namespace CVC4::parser;
  * Parses an expression.
  * @return the parsed expression
  */
-parseExpr returns [CVC4::parser::smt::myExpr expr]
+parseExpr returns [CVC4::parser::smt1::myExpr expr]
   : annotatedFormula[expr]
   | EOF
   ;
@@ -148,6 +148,14 @@ parseExpr returns [CVC4::parser::smt::myExpr expr]
  */
 parseCommand returns [CVC4::Command* cmd = NULL]
   : b = benchmark { $cmd = b; }
+  | LPAREN_TOK c=IDENTIFIER
+    { std::string s = AntlrInput::tokenText($c);
+      if(s == "set" || s == "get") {
+        PARSER_STATE->parseError(std::string("In SMT-LIBv1 mode, expected keyword `benchmark', but it looks like you're writing SMT-LIBv2.  Use --lang smt for SMT-LIBv2."));
+      } else {
+        PARSER_STATE->parseError(std::string("expected keyword `benchmark', got `" + s + "'"));
+      }
+    }
   ;
 
 /**
@@ -521,7 +529,7 @@ sortName[std::string& name, CVC4::parser::DeclarationCheck check]
   : identifier[name,check,SYM_SORT]
   ;
 
-sortSymbol returns [CVC4::parser::smt::myType t]
+sortSymbol returns [CVC4::parser::smt1::myType t]
 @declarations {
   std::string name;
 }
diff --git a/src/parser/smt/smt.cpp b/src/parser/smt1/smt1.cpp
index e554cee10..c91743226 100644
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt1/smt1.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file smt.cpp
+/*! \file smt1.cpp
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: mdeters
@@ -11,7 +11,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** Definitions of SMT constants.
+ ** Definitions of SMT-LIB (v1) constants.
  **/
 
 #include <ext/hash_map>
@@ -22,13 +22,13 @@ namespace std {
 #include "expr/type.h"
 #include "expr/command.h"
 #include "parser/parser.h"
-#include "parser/smt/smt.h"
+#include "parser/smt1/smt1.h"
 
 namespace CVC4 {
 namespace parser {
 
-std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newLogicMap() {
-  std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> logicMap;
+std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> Smt1::newLogicMap() {
+  std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> logicMap;
   logicMap["AUFLIA"] = AUFLIA;
   logicMap["AUFLIRA"] = AUFLIRA;
   logicMap["AUFNIRA"] = AUFNIRA;
@@ -66,12 +66,12 @@ std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newL
   return logicMap;
 }
 
-Smt::Logic Smt::toLogic(const std::string& name) {
-  static std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> logicMap = newLogicMap();
+Smt1::Logic Smt1::toLogic(const std::string& name) {
+  static std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> logicMap = newLogicMap();
   return logicMap[name];
 }
 
-Smt::Smt(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
+Smt1::Smt1(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
   Parser(exprManager,input,strictMode,parseOnly),
   d_logicSet(false) {
 
@@ -87,7 +87,7 @@ Smt::Smt(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly
 
 }
 
-void Smt::addArithmeticOperators() {
+void Smt1::addArithmeticOperators() {
   addOperator(kind::PLUS);
   addOperator(kind::MINUS);
   addOperator(kind::UMINUS);
@@ -98,7 +98,7 @@ void Smt::addArithmeticOperators() {
   addOperator(kind::GEQ);
 }
 
-void Smt::addTheory(Theory theory) {
+void Smt1::addTheory(Theory theory) {
   switch(theory) {
   case THEORY_ARRAYS:
   case THEORY_ARRAYS_EX: {
@@ -171,11 +171,11 @@ void Smt::addTheory(Theory theory) {
   }
 }
 
-bool Smt::logicIsSet() {
+bool Smt1::logicIsSet() {
   return d_logicSet;
 }
 
-void Smt::setLogic(const std::string& name) {
+void Smt1::setLogic(const std::string& name) {
   d_logicSet = true;
   d_logic = toLogic(name);
 
@@ -322,7 +322,7 @@ void Smt::setLogic(const std::string& name) {
     addTheory(THEORY_QUANTIFIERS);
     break;
   }
-}/* Smt::setLogic() */
+}/* Smt1::setLogic() */
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/smt/smt.h b/src/parser/smt1/smt1.h
index 1d550cd7e..f6c99da04 100644
--- a/src/parser/smt/smt.h
+++ b/src/parser/smt1/smt1.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file smt.h
+/*! \file smt1.h
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: mdeters
@@ -16,8 +16,8 @@
 
 #include "cvc4parser_private.h"
 
-#ifndef __CVC4__PARSER__SMT_H
-#define __CVC4__PARSER__SMT_H
+#ifndef __CVC4__PARSER__SMT1_H
+#define __CVC4__PARSER__SMT1_H
 
 #include <ext/hash_map>
 namespace std { using namespace __gnu_cxx; }
@@ -31,7 +31,7 @@ class SExpr;
 
 namespace parser {
 
-class Smt : public Parser {
+class Smt1 : public Parser {
   friend class ParserBuilder;
 
 public:
@@ -92,7 +92,7 @@ private:
   Logic d_logic;
 
 protected:
-  Smt(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
+  Smt1(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
 
 public:
   /**
@@ -117,9 +117,9 @@ private:
 
   void addArithmeticOperators();
   static std::hash_map<const std::string, Logic, CVC4::StringHashFunction> newLogicMap();
-};/* class Smt */
+};/* class Smt1 */
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__PARSER__SMT_H */
+#endif /* __CVC4__PARSER__SMT1_H */
diff --git a/src/parser/smt/smt_input.cpp b/src/parser/smt1/smt1_input.cpp
index 85a117dd0..4987cd793 100644
--- a/src/parser/smt/smt_input.cpp
+++ b/src/parser/smt1/smt1_input.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file smt_input.cpp
+/*! \file smt1_input.cpp
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: mdeters
@@ -18,55 +18,55 @@
 
 #include <antlr3.h>
 
-#include "parser/smt/smt_input.h"
+#include "parser/smt1/smt1_input.h"
 #include "expr/expr_manager.h"
 #include "parser/input.h"
 #include "parser/parser.h"
 #include "parser/parser_exception.h"
-#include "parser/smt/generated/SmtLexer.h"
-#include "parser/smt/generated/SmtParser.h"
+#include "parser/smt1/generated/Smt1Lexer.h"
+#include "parser/smt1/generated/Smt1Parser.h"
 
 namespace CVC4 {
 namespace parser {
 
 /* Use lookahead=2 */
-SmtInput::SmtInput(AntlrInputStream& inputStream) :
+Smt1Input::Smt1Input(AntlrInputStream& inputStream) :
   AntlrInput(inputStream, 2) {
   pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
   AlwaysAssert( input != NULL );
 
-  d_pSmtLexer = SmtLexerNew(input);
-  if( d_pSmtLexer == NULL ) {
+  d_pSmt1Lexer = Smt1LexerNew(input);
+  if( d_pSmt1Lexer == NULL ) {
     throw ParserException("Failed to create SMT lexer.");
   }
 
-  setAntlr3Lexer( d_pSmtLexer->pLexer );
+  setAntlr3Lexer( d_pSmt1Lexer->pLexer );
 
   pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
   AlwaysAssert( tokenStream != NULL );
 
-  d_pSmtParser = SmtParserNew(tokenStream);
-  if( d_pSmtParser == NULL ) {
+  d_pSmt1Parser = Smt1ParserNew(tokenStream);
+  if( d_pSmt1Parser == NULL ) {
     throw ParserException("Failed to create SMT parser.");
   }
 
-  setAntlr3Parser(d_pSmtParser->pParser);
+  setAntlr3Parser(d_pSmt1Parser->pParser);
 }
 
 
-SmtInput::~SmtInput() {
-  d_pSmtLexer->free(d_pSmtLexer);
-  d_pSmtParser->free(d_pSmtParser);
+Smt1Input::~Smt1Input() {
+  d_pSmt1Lexer->free(d_pSmt1Lexer);
+  d_pSmt1Parser->free(d_pSmt1Parser);
 }
 
-Command* SmtInput::parseCommand()
+Command* Smt1Input::parseCommand()
   throw (ParserException, TypeCheckingException, AssertionException) {
-  return d_pSmtParser->parseCommand(d_pSmtParser);
+  return d_pSmt1Parser->parseCommand(d_pSmt1Parser);
 }
 
-Expr SmtInput::parseExpr()
+Expr Smt1Input::parseExpr()
   throw (ParserException, TypeCheckingException, AssertionException) {
-  return d_pSmtParser->parseExpr(d_pSmtParser);
+  return d_pSmt1Parser->parseExpr(d_pSmt1Parser);
 }
 
 }/* CVC4::parser namespace */
diff --git a/src/parser/smt/smt_input.h b/src/parser/smt1/smt1_input.h
index b976a3b6a..77d6f4b50 100644
--- a/src/parser/smt/smt_input.h
+++ b/src/parser/smt1/smt1_input.h
@@ -18,14 +18,14 @@
 
 #include "cvc4parser_private.h"
 
-#ifndef __CVC4__PARSER__SMT_INPUT_H
-#define __CVC4__PARSER__SMT_INPUT_H
+#ifndef __CVC4__PARSER__SMT1_INPUT_H
+#define __CVC4__PARSER__SMT1_INPUT_H
 
 #include "parser/antlr_input.h"
-#include "parser/smt/generated/SmtLexer.h"
-#include "parser/smt/generated/SmtParser.h"
+#include "parser/smt1/generated/Smt1Lexer.h"
+#include "parser/smt1/generated/Smt1Parser.h"
 
-// extern void SmtParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser);
+// extern void Smt1ParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser);
 
 namespace CVC4 {
 
@@ -35,13 +35,13 @@ class ExprManager;
 
 namespace parser {
 
-class SmtInput : public AntlrInput {
+class Smt1Input : public AntlrInput {
 
   /** The ANTLR3 SMT lexer for the input. */
-  pSmtLexer d_pSmtLexer;
+  pSmt1Lexer d_pSmt1Lexer;
 
   /** The ANTLR3 CVC parser for the input. */
-  pSmtParser d_pSmtParser;
+  pSmt1Parser d_pSmt1Parser;
 
 public:
 
@@ -50,14 +50,14 @@ public:
    *
    * @param inputStream the input stream to use
    */
-  SmtInput(AntlrInputStream& inputStream);
+  Smt1Input(AntlrInputStream& inputStream);
 
   /** Destructor. Frees the lexer and the parser. */
-  virtual ~SmtInput();
+  virtual ~Smt1Input();
 
   /** Get the language that this Input is reading. */
   InputLanguage getLanguage() const throw() {
-    return language::input::LANG_SMTLIB;
+    return language::input::LANG_SMTLIB_V1;
   }
 
 protected:
@@ -88,9 +88,9 @@ private:
    */
   void init();
 
-};/* class SmtInput */
+};/* class Smt1Input */
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__PARSER__SMT_INPUT_H */
+#endif /* __CVC4__PARSER__SMT1_INPUT_H */
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 03aa7acc1..fb97d5d1e 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -355,6 +355,16 @@ command returns [CVC4::Command* cmd = NULL]
         PARSER_STATE->parseError("Extended commands are not permitted while operating in strict compliance mode.");
       }
     }
+
+    /* error handling */
+  | SIMPLE_SYMBOL
+    { std::string id = AntlrInput::tokenText($SIMPLE_SYMBOL);
+      if(id == "benchmark") {
+        PARSER_STATE->parseError("In SMT-LIBv2 mode, but got something that looks like SMT-LIBv1.  Use --lang smt1 for SMT-LIBv1.");
+      } else {
+        PARSER_STATE->parseError("expected SMT-LIBv2 command, got `" + id + "'.");
+      }
+    }
   ;
 
 extendedCommand[CVC4::Command*& cmd]
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 9bdadc440..ca7697810 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -19,7 +19,7 @@
 #include "expr/type.h"
 #include "expr/command.h"
 #include "parser/parser.h"
-#include "parser/smt/smt.h"
+#include "parser/smt1/smt1.h"
 #include "parser/smt2/smt2.h"
 
 namespace CVC4 {
@@ -98,107 +98,107 @@ bool Smt2::logicIsSet() {
 
 void Smt2::setLogic(const std::string& name) {
   d_logicSet = true;
-  d_logic = Smt::toLogic(name);
+  d_logic = Smt1::toLogic(name);
 
   // Core theory belongs to every logic
   addTheory(THEORY_CORE);
 
   switch(d_logic) {
-  case Smt::QF_SAT:
+  case Smt1::QF_SAT:
     /* No extra symbols necessary */
     break;
 
-  case Smt::QF_AX:
+  case Smt1::QF_AX:
     addTheory(THEORY_ARRAYS);
     break;
 
-  case Smt::QF_IDL:
-  case Smt::QF_LIA:
-  case Smt::QF_NIA:
+  case Smt1::QF_IDL:
+  case Smt1::QF_LIA:
+  case Smt1::QF_NIA:
     addTheory(THEORY_INTS);
     break;
 
-  case Smt::QF_RDL:
-  case Smt::QF_LRA:
-  case Smt::QF_NRA:
+  case Smt1::QF_RDL:
+  case Smt1::QF_LRA:
+  case Smt1::QF_NRA:
     addTheory(THEORY_REALS);
     break;
 
-  case Smt::QF_UF:
+  case Smt1::QF_UF:
     addOperator(kind::APPLY_UF);
     break;
 
-  case Smt::QF_UFIDL:
-  case Smt::QF_UFLIA:
-  case Smt::QF_UFNIA:// nonstandard logic
+  case Smt1::QF_UFIDL:
+  case Smt1::QF_UFLIA:
+  case Smt1::QF_UFNIA:// nonstandard logic
     addTheory(THEORY_INTS);
     addOperator(kind::APPLY_UF);
     break;
 
-  case Smt::QF_UFLRA:
-  case Smt::QF_UFNRA:
+  case Smt1::QF_UFLRA:
+  case Smt1::QF_UFNRA:
     addTheory(THEORY_REALS);
     addOperator(kind::APPLY_UF);
     break;
 
-  case Smt::QF_UFLIRA:// nonstandard logic
-  case Smt::QF_UFNIRA:// nonstandard logic
+  case Smt1::QF_UFLIRA:// nonstandard logic
+  case Smt1::QF_UFNIRA:// nonstandard logic
     addOperator(kind::APPLY_UF);
     addTheory(THEORY_INTS);
     addTheory(THEORY_REALS);
     break;
 
-  case Smt::QF_BV:
+  case Smt1::QF_BV:
     addTheory(THEORY_BITVECTORS);
     break;
 
-  case Smt::QF_ABV:
+  case Smt1::QF_ABV:
     addTheory(THEORY_ARRAYS);
     addTheory(THEORY_BITVECTORS);
     break;
 
-  case Smt::QF_UFBV:
+  case Smt1::QF_UFBV:
     addOperator(kind::APPLY_UF);
     addTheory(THEORY_BITVECTORS);
     break;
 
-  case Smt::QF_AUFBV:
+  case Smt1::QF_AUFBV:
     addOperator(kind::APPLY_UF);
     addTheory(THEORY_ARRAYS);
     addTheory(THEORY_BITVECTORS);
     break;
 
-  case Smt::QF_AUFBVLIA:
+  case Smt1::QF_AUFBVLIA:
     addOperator(kind::APPLY_UF);
     addTheory(THEORY_ARRAYS);
     addTheory(THEORY_BITVECTORS);
     addTheory(THEORY_INTS);
     break;
 
-  case Smt::QF_AUFBVLRA:
+  case Smt1::QF_AUFBVLRA:
     addOperator(kind::APPLY_UF);
     addTheory(THEORY_ARRAYS);
     addTheory(THEORY_BITVECTORS);
     addTheory(THEORY_REALS);
     break;
 
-  case Smt::QF_AUFLIA:
+  case Smt1::QF_AUFLIA:
     addTheory(THEORY_ARRAYS);
     addOperator(kind::APPLY_UF);
     addTheory(THEORY_INTS);
     break;
 
-  case Smt::QF_AUFLIRA:
+  case Smt1::QF_AUFLIRA:
     addTheory(THEORY_ARRAYS);
     addOperator(kind::APPLY_UF);
     addTheory(THEORY_INTS);
     addTheory(THEORY_REALS);
     break;
 
-  case Smt::ALL_SUPPORTED:
+  case Smt1::ALL_SUPPORTED:
     addTheory(THEORY_QUANTIFIERS);
     /* fall through */
-  case Smt::QF_ALL_SUPPORTED:
+  case Smt1::QF_ALL_SUPPORTED:
     addTheory(THEORY_ARRAYS);
     addOperator(kind::APPLY_UF);
     addTheory(THEORY_INTS);
@@ -206,21 +206,21 @@ void Smt2::setLogic(const std::string& name) {
     addTheory(THEORY_BITVECTORS);
     break;
 
-  case Smt::AUFLIA:
-  case Smt::AUFLIRA:
-  case Smt::AUFNIRA:
-  case Smt::LRA:
-  case Smt::UFNIA:
-  case Smt::UFNIRA:
-  case Smt::UFLRA:
-    if(d_logic != Smt::AUFLIA && d_logic != Smt::UFNIA) {
+  case Smt1::AUFLIA:
+  case Smt1::AUFLIRA:
+  case Smt1::AUFNIRA:
+  case Smt1::LRA:
+  case Smt1::UFNIA:
+  case Smt1::UFNIRA:
+  case Smt1::UFLRA:
+    if(d_logic != Smt1::AUFLIA && d_logic != Smt1::UFNIA) {
       addTheory(THEORY_REALS);
     }
-    if(d_logic != Smt::LRA) {
+    if(d_logic != Smt1::LRA) {
       addOperator(kind::APPLY_UF);
-      if(d_logic != Smt::UFLRA) {
+      if(d_logic != Smt1::UFLRA) {
         addTheory(THEORY_INTS);
-        if(d_logic != Smt::UFNIA && d_logic != Smt::UFNIRA) {
+        if(d_logic != Smt1::UFNIA && d_logic != Smt1::UFNIRA) {
           addTheory(THEORY_ARRAYS);
         }
       }
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 9bd85d7bc..72310b5a4 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -22,7 +22,7 @@
 #define __CVC4__PARSER__SMT2_H
 
 #include "parser/parser.h"
-#include "parser/smt/smt.h"
+#include "parser/smt1/smt1.h"
 
 #include <sstream>
 
@@ -48,7 +48,7 @@ public:
 
 private:
   bool d_logicSet;
-  Smt::Logic d_logic;
+  Smt1::Logic d_logic;
 
 protected:
   Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index ab7ce5422..134498eea 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -18,7 +18,6 @@
 
 #include "expr/type.h"
 #include "parser/parser.h"
-#include "parser/smt/smt.h"
 #include "parser/tptp/tptp.h"
 #include "parser/antlr_input.h"
 
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index ae4ad4e7f..9d75a1d37 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -22,7 +22,6 @@
 #define __CVC4__PARSER__TPTP_H
 
 #include "parser/parser.h"
-#include "parser/smt/smt.h"
 #include "expr/command.h"
 #include <ext/hash_set>