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

33 files changed, 301 insertions, 219 deletions

diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index aa63846cf..6b09fcc27 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -61,13 +61,13 @@ BUILT_SOURCES = \
 
 TOKENS_FILES = \
 	cvc_tokens.h \
-	smt_tokens.h \
+	smt1_tokens.h \
 	smt2_tokens.h \
 	tptp_tokens.h
 
 cvc_tokens.h: @srcdir@/../parser/cvc/Cvc.g
 	$(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9_-][a-zA-Z0-9_-]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9_-]*\)'\''.*/"\1",/' | sort -u >$@
-smt_tokens.h: @srcdir@/../parser/smt/Smt.g
+smt1_tokens.h: @srcdir@/../parser/smt1/Smt1.g
 	$(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9_-][a-zA-Z0-9_-]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9_-]*\)'\''.*/"\1",/' | sort -u >$@
 smt2_tokens.h: @srcdir@/../parser/smt2/Smt2.g
 	$(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9_-][a-zA-Z0-9_-]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9_-]*\)'\''.*/"\1",/' | sort -u >$@
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 20b4c2bc2..a3086d96c 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -153,7 +153,9 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
         opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2);
       } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
-        opts.set(options::inputLanguage, language::input::LANG_SMTLIB);
+        opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V1);
+      } else if(len >= 5 && !strcmp(".smt1", filename + len - 5)) {
+        opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V1);
       } else if((len >= 2 && !strcmp(".p", filename + len - 2))
                 || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
         opts.set(options::inputLanguage, language::input::LANG_TPTP);
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index b0934c0ee..719c8f61d 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -64,9 +64,9 @@ static const std::string cvc_commands[] = {
 #include "main/cvc_tokens.h"
 };/* cvc_commands */
 
-static const std::string smt_commands[] = {
-#include "main/smt_tokens.h"
-};/* smt_commands */
+static const std::string smt1_commands[] = {
+#include "main/smt1_tokens.h"
+};/* smt1_commands */
 
 static const std::string smt2_commands[] = {
 #include "main/smt2_tokens.h"
@@ -105,10 +105,10 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
       commandsBegin = cvc_commands;
       commandsEnd = cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands);
       break;
-    case output::LANG_SMTLIB:
-      d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib";
-      commandsBegin = smt_commands;
-      commandsEnd = smt_commands + sizeof(smt_commands) / sizeof(*smt_commands);
+    case output::LANG_SMTLIB_V1:
+      d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib1";
+      commandsBegin = smt1_commands;
+      commandsEnd = smt1_commands + sizeof(smt1_commands) / sizeof(*smt1_commands);
       break;
     case output::LANG_SMTLIB_V2:
       d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2";
diff --git a/src/main/options b/src/main/options
index 58ea5e544..02c4643b3 100644
--- a/src/main/options
+++ b/src/main/options
@@ -20,7 +20,7 @@ option - --show-trace-tags void :handler CVC4::main::showTraceTags :handler-incl
  show all available tags for tracing
 
 expert-option earlyExit --early-exit bool :default true
- do not run destructors at exit; default on except in debug mode
+ do not run destructors at exit; default on except in debug builds
 
 # portfolio options
 option printWinner bool
diff --git a/src/options/base_options b/src/options/base_options
index cd1bec00a..91b6354d1 100644
--- a/src/options/base_options
+++ b/src/options/base_options
@@ -125,7 +125,8 @@ option - debug -d --debug=TAG argument :handler CVC4::options::addDebugTag
 option printSuccess print-success --print-success bool :predicate CVC4::options::setPrintSuccess :predicate-include "options/base_options_handlers.h"
  print the "success" output required of SMT-LIBv2
 
-alias --smtlib2 = --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental --no-interactive
+alias --smtlib = --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental --no-interactive
  SMT-LIBv2 compliance mode (implies other options)
+undocumented-alias --smtlib2 = --smtlib
 
 endmodule
diff --git a/src/options/base_options_handlers.h b/src/options/base_options_handlers.h
index f29e98a9b..83bcfdf32 100644
--- a/src/options/base_options_handlers.h
+++ b/src/options/base_options_handlers.h
@@ -71,11 +71,16 @@ inline void decreaseVerbosity(std::string option, SmtEngine* smt) {
 }
 
 inline OutputLanguage stringToOutputLanguage(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "cvc4" || optarg == "pl" || optarg == "presentation" || optarg == "LANG_CVC4") {
+  if(optarg == "cvc4" || optarg == "pl" ||
+     optarg == "presentation" || optarg == "native" ||
+     optarg == "LANG_CVC4") {
     return language::output::LANG_CVC4;
-  } else if(optarg == "smtlib" || optarg == "smt" || optarg == "LANG_SMTLIB") {
-    return language::output::LANG_SMTLIB;
-  } else if(optarg == "smtlib2" || optarg == "smt2" || optarg == "LANG_SMTLIB_V2") {
+  } else if(optarg == "smtlib1" || optarg == "smt1" ||
+            optarg == "LANG_SMTLIB_V1") {
+    return language::output::LANG_SMTLIB_V1;
+  } else if(optarg == "smtlib" || optarg == "smt" ||
+            optarg == "smtlib2" || optarg == "smt2" ||
+            optarg == "LANG_SMTLIB_V2") {
     return language::output::LANG_SMTLIB_V2;
   } else if(optarg == "tptp" || optarg == "LANG_TPTP") {
     return language::output::LANG_TPTP;
@@ -86,8 +91,8 @@ inline OutputLanguage stringToOutputLanguage(std::string option, std::string opt
   }
 
   if(optarg != "help") {
-    throw OptionException(std::string("unknown language for ") + option + ": `" +
-                          optarg + "'.  Try --output-lang help.");
+    throw OptionException(std::string("unknown language for ") + option +
+                          ": `" + optarg + "'.  Try --output-lang help.");
   }
 
   options::languageHelp.set(true);
@@ -95,11 +100,16 @@ inline OutputLanguage stringToOutputLanguage(std::string option, std::string opt
 }
 
 inline InputLanguage stringToInputLanguage(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "cvc4" || optarg == "pl" || optarg == "presentation" || optarg == "LANG_CVC4") {
+  if(optarg == "cvc4" || optarg == "pl" ||
+     optarg == "presentation" || optarg == "native" ||
+     optarg == "LANG_CVC4") {
     return language::input::LANG_CVC4;
-  } else if(optarg == "smtlib" || optarg == "smt" || optarg == "LANG_SMTLIB") {
-    return language::input::LANG_SMTLIB;
-  } else if(optarg == "smtlib2" || optarg == "smt2" || optarg == "LANG_SMTLIB_V2") {
+  } else if(optarg == "smtlib1" || optarg == "smt1" ||
+            optarg == "LANG_SMTLIB_V1") {
+    return language::input::LANG_SMTLIB_V1;
+  } else if(optarg == "smtlib" || optarg == "smt" ||
+            optarg == "smtlib2" || optarg == "smt2" ||
+            optarg == "LANG_SMTLIB_V2") {
     return language::input::LANG_SMTLIB_V2;
   } else if(optarg == "tptp" || optarg == "LANG_TPTP") {
     return language::input::LANG_TPTP;
@@ -108,8 +118,8 @@ inline InputLanguage stringToInputLanguage(std::string option, std::string optar
   }
 
   if(optarg != "help") {
-    throw OptionException(std::string("unknown language for ") + option + ": `" +
-                          optarg + "'.  Try --lang help.");
+    throw OptionException(std::string("unknown language for ") + option +
+                          ": `" + optarg + "'.  Try --lang help.");
   }
 
   options::languageHelp.set(true);
diff --git a/src/options/mkoptions b/src/options/mkoptions
index cc581e69c..f023686ad 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -112,6 +112,7 @@ function module {
 
   seen_module=true
   if [ $# -lt 3 -o -z "$1" -o -z "$2" -o -z "$3" ]; then
+    echo >&2
     echo "$kf:$lineno: error: \"module\" directive requires exactly three arguments" >&2
     exit 1
   fi
@@ -144,6 +145,7 @@ function endmodule {
   check_doc
   seen_endmodule=true
   if [ $# -ne 0 ]; then
+    echo >&2
     echo "$kf:$lineno: error: endmodule takes no arguments" >&2
     exit 1
   fi
@@ -223,12 +225,14 @@ function handle_option {
     while [ $i -lt $type_pos ]; do
       if expr "${args[$i]}" : '--' &>/dev/null || expr "${args[$i]}" : '/--' &>/dev/null; then
         if [ -n "$long_option" -o -n "$long_option_alternate" ]; then
+          echo >&2
           echo "$kf:$lineno: error: malformed option line for \`$internal': unexpected \`${args[$i]}'" >&2
           exit 1
         fi
         long_option="$(echo "${args[$i]}" | sed 's,/.*,,')"
         if [ -n "$long_option" ]; then
           if ! expr "$long_option" : '--.' &>/dev/null; then
+            echo >&2
             echo "$kf:$option: bad long option \`$long_option': expected something like \`--foo'" >&2
             exit 1
           fi
@@ -239,6 +243,7 @@ function handle_option {
           long_option_alternate_set=set
           if [ -n "$long_option_alternate" ]; then
             if ! expr "$long_option_alternate" : '--.' &>/dev/null; then
+              echo >&2
               echo "$kf:$option: bad alternate long option \`$long_option_alternate': expected something like \`--foo'" >&2
               exit 1
             fi
@@ -247,12 +252,14 @@ function handle_option {
         fi
       elif expr "${args[$i]}" : '-' &>/dev/null || expr "${args[$i]}" : '/-' &>/dev/null; then
         if [ -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o -n "$long_option_alternate" ]; then
+          echo >&2
           echo "$kf:$lineno: error: malformed option line for \`$internal': unexpected \`${args[$i]}'" >&2
           exit 1
         fi
         short_option="$(echo "${args[$i]}" | sed 's,/.*,,')"
         if [ -n "$short_option" ]; then
           if ! expr "$short_option" : '-.$' &>/dev/null; then
+            echo >&2
             echo "$kf:$option: bad short option \`$short_option': expected something like \`-x'" >&2
             exit 1
           fi
@@ -262,6 +269,7 @@ function handle_option {
           short_option_alternate="$(echo "${args[$i]}" | sed 's,[^/]*/,,')"
           if expr "$short_option_alternate" : - &>/dev/null; then
             if ! expr "$short_option_alternate" : '-.$' &>/dev/null; then
+              echo >&2
               echo "$kf:$option: bad alternate short option \`$short_option_alternate': expected something like \`-x'" >&2
               exit 1
             fi
@@ -270,6 +278,7 @@ function handle_option {
         fi
       else
         if [ -n "$smtname" -o -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o -n "$long_option_alternate" ]; then
+          echo >&2
           echo "$kf:$lineno: error: malformed option line for \`$internal': unexpected \`${args[$i]}'" >&2
           exit 1
         fi
@@ -280,9 +289,11 @@ function handle_option {
   fi
 
   if [ "$type" = void -a "$internal" != - ]; then
+    echo >&2
     echo "$kf:$lineno: error: $internal cannot be void-typed; use \`-' as the name if its to be void" >&2
     exit 1
   elif [ "$type" != void -a "$internal" = - ]; then
+    echo >&2
     echo "$kf:$lineno: error: cannot use an unnamed option if its type is not void" >&2
     exit 1
   fi
@@ -296,9 +307,11 @@ function handle_option {
     long_option_alternate="no-$(echo "$long_option" | sed 's,^--,,')"
   fi
   if [ "$type" != bool -a -n "$short_option_alternate" ]; then
+    echo >&2
     echo "$kf:$lineno: error: cannot use alternate short option -$short_option_alternate for \`$internal' because it's not of bool type" >&2
     exit 1
   elif [ "$type" != bool -a -n "$long_option_alternate" ]; then
+    echo >&2
     echo "$kf:$lineno: error: cannot use alternate long option --$long_option_alternate for \`$internal' because it's not of bool type" >&2
     exit 1
   fi
@@ -306,6 +319,7 @@ function handle_option {
   # check for duplicates
   if [ "$internal" != - ]; then
     if echo " $all_declared_internal_options " | grep -q " $internal "; then
+      echo >&2
       echo "$kf:$lineno: error: internal option name \`$internal' previously declared" >&2
       exit 1
     fi
@@ -313,6 +327,7 @@ function handle_option {
   fi
   if [ -n "$long_option" ]; then
     if echo " $all_declared_long_options " | grep -q " $long_option "; then
+      echo >&2
       echo "$kf:$lineno: error: long option name \`--$long_option' previously declared" >&2
       exit 1
     fi
@@ -320,6 +335,7 @@ function handle_option {
   fi
   if [ -n "$long_option_alternate" ]; then
     if echo " $all_declared_long_options " | grep -q " $long_option_alternate "; then
+      echo >&2
       echo "$kf:$lineno: error: long option name \`--$long_option_alternate' previously declared" >&2
       exit 1
     fi
@@ -327,6 +343,7 @@ function handle_option {
   fi
   if [ -n "$short_option" ]; then
     if echo " $all_declared_short_options " | grep -q " $short_option "; then
+      echo >&2
       echo "$kf:$lineno: error: short option name \`-$short_option' previously declared" >&2
       exit 1
     fi
@@ -334,6 +351,7 @@ function handle_option {
   fi
   if [ -n "$short_option_alternate" ]; then
     if echo " $all_declared_short_options " | grep -q " $short_option_alternate "; then
+      echo >&2
       echo "$kf:$lineno: error: short option name \`-$short_option_alternate' previously declared" >&2
       exit 1
     fi
@@ -341,6 +359,7 @@ function handle_option {
   fi
   if [ -n "$smtname" ]; then
     if echo " $all_declared_smt_options " | grep -q " $smtname "; then
+      echo >&2
       echo "$kf:$lineno: error: SMT option name \`$smtname' previously declared" >&2
       exit 1
     fi
@@ -359,6 +378,7 @@ function handle_option {
     :handler)
        let ++i
        if [ -n "$handlers" ]; then
+         echo >&2
          echo "$kf:$lineno: error: cannot specify more than one handler; maybe you want a :handler and a :predicate" >&2
          exit 1
        fi
@@ -406,6 +426,7 @@ function handle_option {
        readOnly=true
        ;;
     *)
+       echo >&2
        echo "$kf:$lineno: error in option \`$internal': bad attribute \`$attribute'" >&2
        exit 1
     esac
@@ -529,6 +550,7 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r
   if [ "$type" = bool ] && [ -n "$cases" -o -n "$cases_alternate" -o -n "$smtname" ]; then
     run_handlers=
     if [ -n "$handlers" ]; then
+      echo >&2
       echo "$kf:$lineno: error: bool-valued options cannot have handlers" >&2
       exit 1
     fi
@@ -590,6 +612,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
     elif [ -n "$expect_arg" ]; then
       run_handlers=
       if [ -n "$predicates" ]; then
+        echo >&2
         echo "$kf:$lineno: error: void-valued options cannot have predicates" >&2
         exit 1
       fi
@@ -608,6 +631,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
     else
       run_handlers=
       if [ -n "$predicates" ]; then
+        echo >&2
         echo "$kf:$lineno: error: void-valued options cannot have predicates" >&2
         exit 1
       fi
@@ -633,6 +657,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
       break;
 "
     else
+      echo >&2
       echo "$kf:$lineno: internal error: expected BOOL-typed option in alternate handler" >&2
       exit 1
     fi
@@ -790,26 +815,31 @@ function handle_alias {
   expect_doc_alternate=false
 
   if [ $# -lt 3 ]; then
+    echo >&2
     echo "$kf:$lineno: error: malformed \"alias\" command; expected more arguments" >&2
     exit 1
   fi
   if [ "$1" = '=' ]; then
+    echo >&2
     echo "$kf:$lineno: error: malformed \"alias\" command; expected option name" >&2
     exit 1
   fi
   option="$1"
   shift
   if [ "$1" != '=' ]; then
+    echo >&2
     echo "$kf:$lineno: error: malformed \"alias\" command; expected \`='" >&2
     exit 1
   fi
   shift
   if [ $# -eq 0 ]; then
+    echo >&2
     echo "$kf:$lineno: error: malformed \"alias\" command; expected more arguments" >&2
     exit 1
   fi
   cases=
   if ! expr "$option" : - &>/dev/null; then
+    echo >&2
     echo "$kf:$lineno: error: alias for SMT options not yet supported" >&2
     exit 1
   fi
@@ -832,6 +862,7 @@ function handle_alias {
   else
     if ! expr "$option" : '-.$' &>/dev/null; then
       if ! expr "$option" : '-.=' &>/dev/null; then
+        echo >&2
         echo "$kf:$lineno: error: expected short option specification, got \`$option'" >&2
         exit 1
       fi
@@ -884,6 +915,7 @@ function warning {
   check_module_seen
   check_doc
 
+  echo >&2
   echo "$kf:$lineno: warning: $@" >&2
 }
 
@@ -1016,11 +1048,13 @@ function doc-alternate {
   expect_doc_alternate=false
 
   if $expect_doc; then
+    echo >&2
     echo "$kf:$lineno: error: must provide documentation before alternate documentation" >&2
     exit 1
   fi
 
   if [ -z "$short_option_alternate" -a -z "$long_option_alternate" ]; then
+    echo >&2
     echo "$kf:$lineno: cannot document an alternative for option \`$internal'; one does not exist" >&2
     exit 1
   fi
@@ -1100,18 +1134,23 @@ $@"
 function check_doc {
   if $expect_doc; then
     if [ "$internal" != - ]; then
+      echo >&2
       echo "$kf:$lineno: warning: $internal is lacking documentation" >&2
     elif [ -n "$long_option" ]; then
+      echo >&2
       echo "$kf:$lineno: warning: option --$long_option is lacking documentation" >&2
     elif [ -n "$short_option" ]; then
+      echo >&2
       echo "$kf:$lineno: warning: option -$short_option is lacking documentation" >&2
     elif [ -n "$smtname" ]; then
+      echo >&2
       echo "$kf:$lineno: warning: SMT option $smtname is lacking documentation" >&2
     fi
     expect_doc=false
   fi
 
   if $expect_doc_alternate; then
+    echo >&2
     echo "$kf:$lineno: warning: $internal is lacking documentation for the alternative option(s): $short_option_alternate $long_option_alternate" >&2
     expect_doc_alternate=false
   fi
@@ -1119,10 +1158,12 @@ function check_doc {
 
 function check_module_seen {
   if $seen_endmodule; then
+    echo >&2
     echo "$kf:$lineno: error: command after \"endmodule\" declaration (endmodule has to be last)" >&2
     exit 1
   fi
   if ! $seen_module; then
+    echo >&2
     echo "$kf:$lineno: error: no \"module\" declaration found (it has to be first)" >&2
     exit 1
   fi
@@ -1235,7 +1276,7 @@ EOF
     rm -f "$output.tmp"
   else
     mv -f "$output.tmp" "$output"
-    printf "\rregenerated %-60s\n" "$output"
+    printf "\rregenerated %-68s\n" "$output"
   fi
 }
 
@@ -1272,6 +1313,7 @@ while [ $# -gt 0 ]; do
     elif expr "$line" : '\.[ 	]*$' &>/dev/null; then
       doc ""
     elif expr "$line" : '\.' &>/dev/null; then
+      echo >&2
       echo "$kf:$lineno: error: malformed line during processing of option \`$internal': continuation lines should not have content" >&2
       exit 1
     elif expr "$line" : '/.*' &>/dev/null; then
@@ -1279,16 +1321,19 @@ while [ $# -gt 0 ]; do
     else
       line="$(echo "$line" | sed 's,\([<>&()!?*]\),\\\1,g')"
       if ! eval "$line"; then
+        echo >&2
         echo "$kf:$lineno: error was due to evaluation of this line" >&2
         exit 1
       fi
     fi
   done < "$kf"
   if ! $seen_module; then
+    echo >&2
     echo "$kf: error: no module content found in file!" >&2
     exit 1
   fi
   if ! $seen_endmodule; then
+    echo >&2
     echo "$kf:$lineno: error: no \"endmodule\" declaration found (it is required at the end)" >&2
     exit 1
   fi
@@ -1412,7 +1457,7 @@ cat "$output.working"
 
 rm -f "$output.working"
 rm -f "$output.sed"
-diff -q "$output" "$output.tmp" &>/dev/null || (mv -f "$output.tmp" "$output" && printf "\rregenerated %-60s\n" "$output")
+diff -q "$output" "$output.tmp" &>/dev/null || (mv -f "$output.tmp" "$output" && printf "\rregenerated %-68s\n" "$output")
 rm -f "$output.tmp"
 progress "$output" $count $total
 
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index dd8a7af57..63ab085b1 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -233,19 +233,19 @@ static const std::string optionsFootnote = "\n\
 
 static const std::string languageDescription = "\
 Languages currently supported as arguments to the -L / --lang option:\n\
-  auto           attempt to automatically determine the input language\n\
-  pl | cvc4      CVC4 presentation language\n\
-  smt | smtlib   SMT-LIB format 1.2\n\
-  smt2 | smtlib2 SMT-LIB format 2.0\n\
-  tptp           TPTP format (cnf and fof)\n\
+  auto                           attempt to automatically determine language\n\
+  cvc4 | presentation | pl       CVC4 presentation language\n\
+  smt1 | smtlib1                 SMT-LIB format 1.2\n\
+  smt | smtlib | smt2 | smtlib2  SMT-LIB format 2.0\n\
+  tptp                           TPTP format (cnf and fof)\n\
 \n\
 Languages currently supported as arguments to the --output-lang option:\n\
-  auto           match the output language to the input language\n\
-  pl | cvc4      CVC4 presentation language\n\
-  smt | smtlib   SMT-LIB format 1.2\n\
-  smt2 | smtlib2 SMT-LIB format 2.0\n\
-  tptp           TPTP format\n\
-  ast            internal format (simple syntax-tree language)\n\
+  auto                           match output language to input language\n\
+  cvc4 | presentation | pl       CVC4 presentation language\n\
+  smt1 | smtlib1                 SMT-LIB format 1.2\n\
+  smt | smtlib | smt2 | smtlib2  SMT-LIB format 2.0\n\
+  tptp                           TPTP format\n\
+  ast                            internal format (simple syntax trees)\n\
 ";
 
 std::string Options::getDescription() const {
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>
 
diff --git a/src/printer/Makefile.am b/src/printer/Makefile.am
index 7a6ef1158..bb94d75de 100644
--- a/src/printer/Makefile.am
+++ b/src/printer/Makefile.am
@@ -12,8 +12,8 @@ libprinter_la_SOURCES = \
 	dagification_visitor.cpp \
 	ast/ast_printer.h \
 	ast/ast_printer.cpp \
-	smt/smt_printer.h \
-	smt/smt_printer.cpp \
+	smt1/smt1_printer.h \
+	smt1/smt1_printer.cpp \
 	smt2/smt2_printer.h \
 	smt2/smt2_printer.cpp \
 	cvc/cvc_printer.h \
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();
diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt1/smt1_printer.cpp
index bc61368c1..553692dc5 100644
--- a/src/printer/smt/smt_printer.cpp
+++ b/src/printer/smt1/smt1_printer.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file smt_printer.cpp
+/*! \file smt1_printer.cpp
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
@@ -16,7 +16,7 @@
  ** The pretty-printer interface for the SMT output language.
  **/
 
-#include "printer/smt/smt_printer.h"
+#include "printer/smt1/smt1_printer.h"
 #include "expr/expr.h" // for ExprSetDepth etc..
 #include "util/language.h" // for LANG_AST
 #include "expr/node_manager.h" // for VarNameAttr
@@ -31,31 +31,31 @@ using namespace std;
 
 namespace CVC4 {
 namespace printer {
-namespace smt {
+namespace smt1 {
 
-void SmtPrinter::toStream(std::ostream& out, TNode n,
-                          int toDepth, bool types, size_t dag) const throw() {
+void Smt1Printer::toStream(std::ostream& out, TNode n,
+                           int toDepth, bool types, size_t dag) const throw() {
   n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2);
-}/* SmtPrinter::toStream() */
+}/* Smt1Printer::toStream() */
 
-void SmtPrinter::toStream(std::ostream& out, const Command* c,
-                          int toDepth, bool types, size_t dag) const throw() {
+void Smt1Printer::toStream(std::ostream& out, const Command* c,
+                           int toDepth, bool types, size_t dag) const throw() {
   c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2);
-}/* SmtPrinter::toStream() */
+}/* Smt1Printer::toStream() */
 
-void SmtPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() {
+void Smt1Printer::toStream(std::ostream& out, const CommandStatus* s) const throw() {
   s->toStream(out, language::output::LANG_SMTLIB_V2);
-}/* SmtPrinter::toStream() */
+}/* Smt1Printer::toStream() */
 
-void SmtPrinter::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
+void Smt1Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
   Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr);
-}/* SmtPrinter::toStream() */
+}/* Smt1Printer::toStream() */
 
-void SmtPrinter::toStream(std::ostream& out, Model* m, const Command* c) const throw() {
+void Smt1Printer::toStream(std::ostream& out, Model* m, const Command* c) const throw() {
   Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, m, c);
 }
 
-}/* CVC4::printer::smt namespace */
+}/* CVC4::printer::smt1 namespace */
 }/* CVC4::printer namespace */
 }/* CVC4 namespace */
 
diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt1/smt1_printer.h
index a3d62a287..d1b36208c 100644
--- a/src/printer/smt/smt_printer.h
+++ b/src/printer/smt1/smt1_printer.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file smt_printer.h
+/*! \file smt1_printer.h
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
@@ -18,8 +18,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PRINTER__SMT_PRINTER_H
-#define __CVC4__PRINTER__SMT_PRINTER_H
+#ifndef __CVC4__PRINTER__SMT1_PRINTER_H
+#define __CVC4__PRINTER__SMT1_PRINTER_H
 
 #include <iostream>
 
@@ -27,9 +27,9 @@
 
 namespace CVC4 {
 namespace printer {
-namespace smt {
+namespace smt1 {
 
-class SmtPrinter : public CVC4::Printer {
+class Smt1Printer : public CVC4::Printer {
 public:
   void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
@@ -37,11 +37,11 @@ public:
   void toStream(std::ostream& out, const SExpr& sexpr) const throw();
   //for models
   void toStream(std::ostream& out, Model* m, const Command* c) const throw();
-};/* class SmtPrinter */
+};/* class Smt1Printer */
 
-}/* CVC4::printer::smt namespace */
+}/* CVC4::printer::smt1 namespace */
 }/* CVC4::printer namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__PRINTER__SMT_PRINTER_H */
+#endif /* __CVC4__PRINTER__SMT1_PRINTER_H */
 
diff --git a/src/util/language.cpp b/src/util/language.cpp
index 1792797cf..22e9840d7 100644
--- a/src/util/language.cpp
+++ b/src/util/language.cpp
@@ -23,7 +23,7 @@ namespace language {
 
 InputLanguage toInputLanguage(OutputLanguage language) {
   switch(language) {
-  case output::LANG_SMTLIB:
+  case output::LANG_SMTLIB_V1:
   case output::LANG_SMTLIB_V2:
   case output::LANG_TPTP:
   case output::LANG_CVC4:
@@ -41,7 +41,7 @@ InputLanguage toInputLanguage(OutputLanguage language) {
 
 OutputLanguage toOutputLanguage(InputLanguage language) {
   switch(language) {
-  case input::LANG_SMTLIB:
+  case input::LANG_SMTLIB_V1:
   case input::LANG_SMTLIB_V2:
   case input::LANG_CVC4:
   case input::LANG_TPTP:
diff --git a/src/util/language.h b/src/util/language.h
index b84d45d89..867c61be3 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -44,8 +44,8 @@ enum CVC4_PUBLIC Language {
   // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE,
   // INCLUDE IT HERE
 
-  /** The SMTLIB input language */
-  LANG_SMTLIB = 0,
+  /** The SMTLIB v1 input language */
+  LANG_SMTLIB_V1 = 0,
   /** The SMTLIB v2 input language */
   LANG_SMTLIB_V2,
   /** The TPTP input language */
@@ -66,8 +66,8 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_AUTO:
     out << "LANG_AUTO";
     break;
-  case LANG_SMTLIB:
-    out << "LANG_SMTLIB";
+  case LANG_SMTLIB_V1:
+    out << "LANG_SMTLIB_V1";
     break;
   case LANG_SMTLIB_V2:
     out << "LANG_SMTLIB_V2";
@@ -101,8 +101,8 @@ enum CVC4_PUBLIC Language {
   // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE,
   // INCLUDE IT HERE
 
-  /** The SMTLIB output language */
-  LANG_SMTLIB = input::LANG_SMTLIB,
+  /** The SMTLIB v1 output language */
+  LANG_SMTLIB_V1 = input::LANG_SMTLIB_V1,
   /** The SMTLIB v2 output language */
   LANG_SMTLIB_V2 = input::LANG_SMTLIB_V2,
   /** The TPTP output language */
@@ -123,8 +123,8 @@ enum CVC4_PUBLIC Language {
 inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC;
 inline std::ostream& operator<<(std::ostream& out, Language lang) {
   switch(lang) {
-  case LANG_SMTLIB:
-    out << "LANG_SMTLIB";
+  case LANG_SMTLIB_V1:
+    out << "LANG_SMTLIB_V1";
     break;
   case LANG_SMTLIB_V2:
     out << "LANG_SMTLIB_V2";
diff --git a/test/regress/run_regression b/test/regress/run_regression
index 5ed43d1a0..97941653c 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -57,7 +57,7 @@ function gettemp {
 tmpbenchmark=
 if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
   proof_command=PROOFS-NOT-SUPPORTED-IN-SMTLIB-V1
-  lang=smt
+  lang=smt1
   if test -e "$benchmark.expect"; then
     expected_proof=`grep -q '^% PROOF' "$benchmark.expect" && echo yes`
     expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'`
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 01879ec49..bfa2ddc44 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -282,11 +282,11 @@ public:
   }
 };/* class Cvc4ParserTest */
 
-class SmtParserTest : public CxxTest::TestSuite, public ParserBlack {
+class Smt1ParserTest : public CxxTest::TestSuite, public ParserBlack {
   typedef ParserBlack super;
 
 public:
-  SmtParserTest() : ParserBlack(LANG_SMTLIB) { }
+  Smt1ParserTest() : ParserBlack(LANG_SMTLIB_V1) { }
 
   void setUp() {
     super::setUp();
@@ -296,7 +296,7 @@ public:
     super::tearDown();
   }
 
-  void testGoodSmtInputs() {
+  void testGoodSmt1Inputs() {
     tryGoodInput(""); // empty string is OK
     tryGoodInput("(benchmark foo :assumption true)");
     tryGoodInput("(benchmark bar :formula true)");
@@ -309,7 +309,7 @@ public:
     tryGoodInput("; a comment\n(benchmark foo ; hello\n  :formula true; goodbye\n)");
   }
 
-  void testBadSmtInputs() {
+  void testBadSmt1Inputs() {
 // competition builds don't do any checking
 #ifndef CVC4_COMPETITION_MODE
     tryBadInput("(benchmark foo)"); // empty benchmark is not OK
@@ -320,7 +320,7 @@ public:
 #endif /* ! CVC4_COMPETITION_MODE */
   }
 
-  void testGoodSmtExprs() {
+  void testGoodSmt1Exprs() {
     tryGoodExpr("(and a b)");
     tryGoodExpr("(or (and a b) c)");
     tryGoodExpr("(implies (and (implies a b) a) b)");
@@ -333,7 +333,7 @@ public:
     tryGoodExpr("1.5");
   }
 
-  void testBadSmtExprs() {
+  void testBadSmt1Exprs() {
 // competition builds don't do any checking
 #ifndef CVC4_COMPETITION_MODE
     tryBadExpr("(and)"); // wrong arity
@@ -349,7 +349,7 @@ public:
     tryBadExpr("1."); // rational constants must have fractional suffix
 #endif /* ! CVC4_COMPETITION_MODE */
   }
-};/* class SmtParserTest */
+};/* class Smt1ParserTest */
 
 class Smt2ParserTest : public CxxTest::TestSuite, public ParserBlack {
   typedef ParserBlack super;