From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 23 Oct 2014 07:11:18 +0000 (-0400)
Subject: Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.
X-Git-Tag: cvc5-1.0.0~6544
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c6436566dec99c0ed6794fa34b9b67a7e47918b0;p=cvc5.git

Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.

* support for new commands meta-info, declare-const, echo, get-model,
  reset, and reset-assertions
* support for set-option :global-declarations
* support for set-option :produce-assertions
* support for set-option :reproducible-resource-limit
* support for get-info :assertion-stack-levels
* support for set-info :smt-lib-version 2.5
* ascribe types for abstract values (the new 2.5 standard clarifies that
  this is required)
* SMT-LIB v2.5 string literals (we still support 2.0 string literals when
  in 2.0 mode)

What's still to do:
* check-sat-assumptions/get-unsat-assumptions (still being hotly debated).
  Also set-option :produce-unsat-assumptions.
* define-fun-rec doesn't allow mutual recursion
* All options should be restored to defaults with (reset) command.
  (Currently :incremental and maybe others get "stuck" due to late driver
  integration.)
---

diff --git a/NEWS b/NEWS
index 7e3a30d74..89ea1c265 100644
--- a/NEWS
+++ b/NEWS
@@ -7,6 +7,12 @@ Changes since 1.4
 * Simplification mode "incremental" no longer supported.
 * Support for array constants in constraints.
 * Syntax for array models have changed in some language front-ends.
+* New input/output languages supported: "smt2.0" and "smtlib2.0" to
+  force SMT-LIB v2.0; "smt2.5" and "smtlib2.5" to force SMT-LIB v2.5.
+  "smt", "smtlib", "smt2", and "smtlib2" all refer to the current standard
+  version 2.0.  If an :smt-lib-version is set in the input, that overrides
+  the command line.
+* Abstract values in SMT-LIB models are now ascribed types (with "as").
 * In SMT-LIB model output, real-sorted but integer-valued constants are
   now printed in accordance with the standard (e.g. "1.0").
 
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index c976588d4..be1b06cb8 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -385,6 +385,29 @@ std::string ResetCommand::getCommandName() const throw() {
   return "reset";
 }
 
+/* class ResetAssertionsCommand */
+
+void ResetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    smtEngine->resetAssertions();
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+Command* ResetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  return new ResetAssertionsCommand();
+}
+
+Command* ResetAssertionsCommand::clone() const {
+  return new ResetAssertionsCommand();
+}
+
+std::string ResetAssertionsCommand::getCommandName() const throw() {
+  return "reset-assertions";
+}
+
 /* class QuitCommand */
 
 void QuitCommand::invoke(SmtEngine* smtEngine) throw() {
diff --git a/src/expr/command.h b/src/expr/command.h
index 75cf80aae..c4f2fc1bc 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -807,6 +807,16 @@ public:
   std::string getCommandName() const throw();
 };/* class ResetCommand */
 
+class CVC4_PUBLIC ResetAssertionsCommand : public Command {
+public:
+  ResetAssertionsCommand() throw() {}
+  ~ResetAssertionsCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
+  std::string getCommandName() const throw();
+};/* class ResetAssertionsCommand */
+
 class CVC4_PUBLIC QuitCommand : public Command {
 public:
   QuitCommand() throw() {}
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index c5e8e77de..d769ed109 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -985,7 +985,7 @@ inline std::ostream& operator<<(std::ostream& out, ExprDag d) {
  * Use like this:
  *
  *   // let out be an ostream, e an Expr
- *   out << Expr::setlanguage(LANG_SMTLIB_V2) << e << endl;
+ *   out << Expr::setlanguage(LANG_SMTLIB_V2_5) << e << endl;
  *
  * The setting stays permanently (until set again) with the stream.
  */
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 6e10c9a8a..610902270 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -63,7 +63,7 @@ CommandExecutorPortfolio::CommandExecutorPortfolio
   d_stats.registerStat_(&d_statLastWinner);
   d_stats.registerStat_(&d_statWaitTime);
 
-  /* Duplication, Individualisation */
+  /* Duplication, individualization */
   d_exprMgrs.push_back(&d_exprMgr);
   for(unsigned i = 1; i < d_numThreads; ++i) {
     d_exprMgrs.push_back(new ExprManager(d_threadOptions[i]));
@@ -202,6 +202,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
             dynamic_cast<GetAssignmentCommand*>(cmd) != NULL ||
             dynamic_cast<GetModelCommand*>(cmd) != NULL ||
             dynamic_cast<GetProofCommand*>(cmd) != NULL ||
+            dynamic_cast<GetInstantiationsCommand*>(cmd) != NULL ||
             dynamic_cast<GetUnsatCoreCommand*>(cmd) != NULL ||
             dynamic_cast<GetAssertionsCommand*>(cmd) != NULL ||
             dynamic_cast<GetInfoCommand*>(cmd) != NULL ||
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 5fbd5aff5..f9b222b2b 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -35,9 +35,11 @@
 #include "util/configuration.h"
 #include "options/options.h"
 #include "main/command_executor.h"
-# ifdef PORTFOLIO_BUILD
-#    include "main/command_executor_portfolio.h"
-# endif
+
+#ifdef PORTFOLIO_BUILD
+#  include "main/command_executor_portfolio.h"
+#endif
+
 #include "main/options.h"
 #include "smt/options.h"
 #include "util/output.h"
@@ -185,7 +187,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     } else {
       unsigned len = strlen(filename);
       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
-        opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2);
+        opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2_5);
       } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
         opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V1);
       } else if(len >= 5 && !strcmp(".smt1", filename + len - 5)) {
@@ -373,6 +375,10 @@ int runCvc4(int argc, char* argv[], Options& opts) {
           }
           status = pExecutor->doCommand(cmd);
           needReset = true;
+        } else if(dynamic_cast<ResetCommand*>(cmd) != NULL) {
+          pExecutor->doCommand(cmd);
+          allCommands.clear();
+          allCommands.push_back(vector<Command*>());
         } else {
           // We shouldn't copy certain commands, because they can cause
           // an error on replay since there's no associated sat/unsat check
@@ -382,7 +388,10 @@ int runCvc4(int argc, char* argv[], Options& opts) {
              dynamic_cast<GetValueCommand*>(cmd) == NULL &&
              dynamic_cast<GetModelCommand*>(cmd) == NULL &&
              dynamic_cast<GetAssignmentCommand*>(cmd) == NULL &&
-             dynamic_cast<GetInstantiationsCommand*>(cmd) == NULL) {
+             dynamic_cast<GetInstantiationsCommand*>(cmd) == NULL &&
+             dynamic_cast<GetAssertionsCommand*>(cmd) == NULL &&
+             dynamic_cast<GetInfoCommand*>(cmd) == NULL &&
+             dynamic_cast<GetOptionCommand*>(cmd) == NULL) {
             Command* copy = cmd->clone();
             allCommands.back().push_back(copy);
           }
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index bdc956535..0aee195e4 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -123,7 +123,8 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
       commandsBegin = smt1_commands;
       commandsEnd = smt1_commands + sizeof(smt1_commands) / sizeof(*smt1_commands);
       break;
-    case output::LANG_SMTLIB_V2:
+    case output::LANG_SMTLIB_V2_0:
+    case output::LANG_SMTLIB_V2_5:
       d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2";
       commandsBegin = smt2_commands;
       commandsEnd = smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands);
@@ -323,7 +324,8 @@ restart:
     line += "\n";
     goto restart;
   } catch(ParserException& pe) {
-    if(d_options[options::outputLanguage] == output::LANG_SMTLIB_V2) {
+    if(d_options[options::outputLanguage] == output::LANG_SMTLIB_V2_0 ||
+       d_options[options::outputLanguage] == output::LANG_SMTLIB_V2_5) {
       d_out << "(error \"" << pe << "\")" << endl;
     } else {
       d_out << pe << endl;
diff --git a/src/main/main.cpp b/src/main/main.cpp
index ca7266b59..a70c3c7c3 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -65,7 +65,8 @@ int main(int argc, char* argv[]) {
 #ifdef CVC4_COMPETITION_MODE
     *opts[options::out] << "unknown" << endl;
 #endif
-    if(opts[options::outputLanguage] == output::LANG_SMTLIB_V2) {
+    if(opts[options::outputLanguage] == output::LANG_SMTLIB_V2_0 ||
+       opts[options::outputLanguage] == output::LANG_SMTLIB_V2_5) {
       *opts[options::err] << "(error \"" << e << "\")" << endl;
     } else {
       *opts[options::err] << "CVC4 Error:" << endl << e << endl;
diff --git a/src/main/options b/src/main/options
index 6cc6a0ca0..18cc08ed7 100644
--- a/src/main/options
+++ b/src/main/options
@@ -41,6 +41,8 @@ option fallbackSequential  --fallback-sequential bool :default false
 option incrementalParallel --incremental-parallel bool :default false :link --incremental
  Use parallel solver even in incremental mode (may print 'unknown's at times)
 
+option interactive : --interactive bool :read-write
+ force interactive/non-interactive mode
 undocumented-option interactivePrompt /--no-interactive-prompt bool :default true
  turn off interactive prompting while in interactive mode
 
diff --git a/src/options/options.h b/src/options/options.h
index b41c9a66e..092fbe507 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -69,6 +69,8 @@ public:
   Options(const Options& options);
   ~Options();
 
+  Options& operator=(const Options& options);
+
   /**
    * Set the value of the given option.  Use of this default
    * implementation causes a compile-time error; write-able
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index bd723e380..f6c6846e5 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -226,6 +226,14 @@ Options::~Options() {
   delete d_holder;
 }
 
+Options& Options::operator=(const Options& options) {
+  if(this != &options) {
+    delete d_holder;
+    d_holder = new options::OptionsHolder(*options.d_holder);
+  }
+  return *this;
+}
+
 options::OptionsHolder::OptionsHolder() : ${all_modules_defaults}
 {
 }
@@ -253,7 +261,9 @@ Languages currently supported as arguments to the -L / --lang option:\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\
+  smt | smtlib | smt2 |\n\
+    smt2.0 | smtlib2 | smtlib2.0 SMT-LIB format 2.0\n\
+  smt2.5 | smtlib2.5             SMT-LIB format 2.5\n\
   tptp                           TPTP format (cnf and fof)\n\
 \n\
 Languages currently supported as arguments to the --output-lang option:\n\
@@ -261,7 +271,9 @@ Languages currently supported as arguments to the --output-lang option:\n\
   cvc4 | presentation | pl       CVC4 presentation language\n\
   cvc3                           CVC3 presentation language\n\
   smt1 | smtlib1                 SMT-LIB format 1.2\n\
-  smt | smtlib | smt2 | smtlib2  SMT-LIB format 2.0\n\
+  smt | smtlib | smt2 |\n\
+    smt2.0 | smtlib2.0 | smtlib2   SMT-LIB format 2.0\n\
+  smt2.5 | smtlib2.5             SMT-LIB format 2.5\n\
   z3str                          SMT-LIB 2.0 with Z3-str string constraints\n\
   tptp                           TPTP format\n\
   ast                            internal format (simple syntax trees)\n\
@@ -314,7 +326,7 @@ static struct option cmdlineOptions[] = {${all_modules_long_options}
   { NULL, no_argument, NULL, '\0' }
 };/* cmdlineOptions */
 
-#line 318 "${template}"
+#line 322 "${template}"
 
 static void preemptGetopt(int& argc, char**& argv, const char* opt) {
   const size_t maxoptlen = 128;
@@ -507,7 +519,7 @@ std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) thro
     switch(c) {
 ${all_modules_option_handlers}
 
-#line 511 "${template}"
+#line 515 "${template}"
 
     case ':':
       // This can be a long or short option, and the way to get at the
@@ -576,7 +588,7 @@ std::string Options::suggestCommandLineOptions(const std::string& optionName) th
 
 static const char* smtOptions[] = {
   ${all_modules_smt_options},
-#line 580 "${template}"
+#line 584 "${template}"
   NULL
 };/* smtOptions[] */
 
@@ -598,7 +610,7 @@ SExpr Options::getOptions() const throw() {
 
   ${all_modules_get_options}
 
-#line 602 "${template}"
+#line 606 "${template}"
 
   return SExpr(opts);
 }
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index aa431ef42..f8730e372 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -201,8 +201,9 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre
     input = new Smt1Input(inputStream);
     break;
 
-  case LANG_SMTLIB_V2:
-    input = new Smt2Input(inputStream);
+  case LANG_SMTLIB_V2_0:
+  case LANG_SMTLIB_V2_5:
+    input = new Smt2Input(inputStream, lang);
     break;
 
   case LANG_TPTP:
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index ead8caa20..2b442015a 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -702,6 +702,11 @@ mainCommand[CVC4::Command*& cmd]
       PARSER_STATE->reset();
     }
 
+  | RESET_TOK ASSERTIONS_TOK
+    { cmd = new ResetAssertionsCommand();
+      PARSER_STATE->reset();
+    }
+
     // Datatypes can be mututally-recursive if they're in the same
     // definition block, separated by a comma.  So we parse everything
     // and then ask the ExprManager to resolve everything in one go.
diff --git a/src/parser/options b/src/parser/options
index c80914596..66e95889f 100644
--- a/src/parser/options
+++ b/src/parser/options
@@ -14,6 +14,9 @@ option memoryMap --mmap bool
 option semanticChecks /--no-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--no-type-checking
  disable ALL semantic checks, including type checks
 
+option globalDeclarations global-declarations bool :default false
+ force all declarations and definitions to be global
+
 # this is to support security in the online version, and in other similar contexts
 # (--no-include-file disables filesystem access in TPTP and SMT2 parsers)
 # the name --no-include-file is legacy: it also now limits any filesystem access
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 064379cf3..045cd4ae1 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -29,7 +29,6 @@
 #include "expr/kind.h"
 #include "expr/type.h"
 #include "util/output.h"
-#include "options/options.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -43,6 +42,7 @@ Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool par
   d_symtabAllocated(),
   d_symtab(&d_symtabAllocated),
   d_assertionLevel(0),
+  d_globalDeclarations(false),
   d_anonymousFunctionCount(0),
   d_done(false),
   d_checksEnabled(true),
@@ -142,6 +142,9 @@ bool Parser::isPredicate(const std::string& name) {
 
 Expr
 Parser::mkVar(const std::string& name, const Type& type, uint32_t flags) {
+  if(d_globalDeclarations) {
+    flags |= ExprManager::VAR_FLAG_GLOBAL;
+  }
   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
   Expr expr = d_exprManager->mkVar(name, type, flags);
   defineVar(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL);
@@ -158,6 +161,9 @@ Parser::mkBoundVar(const std::string& name, const Type& type) {
 
 Expr
 Parser::mkFunction(const std::string& name, const Type& type, uint32_t flags) {
+  if(d_globalDeclarations) {
+    flags |= ExprManager::VAR_FLAG_GLOBAL;
+  }
   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
   Expr expr = d_exprManager->mkVar(name, type, flags);
   defineFunction(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL);
@@ -166,6 +172,9 @@ Parser::mkFunction(const std::string& name, const Type& type, uint32_t flags) {
 
 Expr
 Parser::mkAnonymousFunction(const std::string& prefix, const Type& type, uint32_t flags) {
+  if(d_globalDeclarations) {
+    flags |= ExprManager::VAR_FLAG_GLOBAL;
+  }
   stringstream name;
   name << prefix << "_anon_" << ++d_anonymousFunctionCount;
   return d_exprManager->mkVar(name.str(), type, flags);
@@ -173,6 +182,9 @@ Parser::mkAnonymousFunction(const std::string& prefix, const Type& type, uint32_
 
 std::vector<Expr>
 Parser::mkVars(const std::vector<std::string> names, const Type& type, uint32_t flags) {
+  if(d_globalDeclarations) {
+    flags |= ExprManager::VAR_FLAG_GLOBAL;
+  }
   std::vector<Expr> vars;
   for(unsigned i = 0; i < names.size(); ++i) {
     vars.push_back(mkVar(names[i], type, flags));
@@ -234,6 +246,9 @@ Parser::defineParameterizedType(const std::string& name,
 
 SortType
 Parser::mkSort(const std::string& name, uint32_t flags) {
+  if(d_globalDeclarations) {
+    flags |= ExprManager::VAR_FLAG_GLOBAL;
+  }
   Debug("parser") << "newSort(" << name << ")" << std::endl;
   Type type = d_exprManager->mkSort(name, flags);
   defineType(name, type);
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 52236294a..ffe33a980 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -133,6 +133,12 @@ class CVC4_PUBLIC Parser {
    */
   size_t d_assertionLevel;
 
+  /**
+   * Whether we're in global declarations mode (all definitions and
+   * declarations are global).
+   */
+  bool d_globalDeclarations;
+
   /**
    * Maintains a list of reserved symbols at the assertion level that might
    * not occur in our symbol table.  This is necessary to e.g. support the
@@ -561,10 +567,14 @@ public:
     }
   }
 
-  inline void reset() {
+  virtual void reset() {
     d_symtab->reset();
   }
 
+  void setGlobalDeclarations(bool flag) {
+    d_globalDeclarations = flag;
+  }
+
   /**
    * Set the current symbol table used by this parser.
    * From now on, this parser will perform its definitions and
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index b467acfeb..241c9c815 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -89,7 +89,8 @@ Parser* ParserBuilder::build()
   case language::input::LANG_SMTLIB_V1:
     parser = new Smt1(d_exprManager, input, d_strictMode, d_parseOnly);
     break;
-  case language::input::LANG_SMTLIB_V2:
+  case language::input::LANG_SMTLIB_V2_0:
+  case language::input::LANG_SMTLIB_V2_5:
     parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly);
     break;
   case language::input::LANG_TPTP:
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 3d57eebff..9281b19f2 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -234,20 +234,22 @@ command returns [CVC4::Command* cmd = NULL]
       }
       PARSER_STATE->setLogic(name);
       $cmd = new SetBenchmarkLogicCommand(name); }
-  | SET_INFO_TOK KEYWORD symbolicExpr[sexpr]
-    { name = AntlrInput::tokenText($KEYWORD);
-      if(name == ":cvc4-logic" || name == ":cvc4_logic") {
-        PARSER_STATE->setLogic(sexpr.getValue());
-      }
-      PARSER_STATE->setInfo(name.c_str() + 1, sexpr);
-      cmd = new SetInfoCommand(name.c_str() + 1, sexpr); }
+  | /* set-info */
+    SET_INFO_TOK metaInfoInternal[cmd]
   | /* get-info */
     GET_INFO_TOK KEYWORD
     { cmd = new GetInfoCommand(AntlrInput::tokenText($KEYWORD).c_str() + 1); }
   | /* set-option */
     SET_OPTION_TOK keyword[name] symbolicExpr[sexpr]
     { PARSER_STATE->setOption(name.c_str() + 1, sexpr);
-      cmd = new SetOptionCommand(name.c_str() + 1, sexpr); }
+      cmd = new SetOptionCommand(name.c_str() + 1, sexpr);
+      // Ugly that this changes the state of the parser; but
+      // global-declarations affects parsing, so we can't hold off
+      // on this until some SmtEngine eventually (if ever) executes it.
+      if(name == ":global-declarations") {
+        PARSER_STATE->setGlobalDeclarations(sexpr.getValue() == "true");
+      }
+    }
   | /* get-option */
     GET_OPTION_TOK KEYWORD
     { cmd = new GetOptionCommand(AntlrInput::tokenText($KEYWORD).c_str() + 1); }
@@ -443,9 +445,18 @@ command returns [CVC4::Command* cmd = NULL]
           cmd = new PopCommand();
         }
       } )
+
+    /* exit */
   | EXIT_TOK
     { cmd = new QuitCommand(); }
 
+    /* New SMT-LIB 2.5 command set */
+  | smt25Command[cmd]
+    { if(PARSER_STATE->v2_0() && PARSER_STATE->strictModeEnabled()) {
+        PARSER_STATE->parseError("SMT-LIB 2.5 commands are not permitted while operating in strict compliance mode and in SMT-LIB 2.0 mode.");
+      }
+    }
+
     /* CVC4-extended SMT-LIB commands */
   | extendedCommand[cmd]
     { if(PARSER_STATE->strictModeEnabled()) {
@@ -464,25 +475,56 @@ command returns [CVC4::Command* cmd = NULL]
     }
   ;
 
-extendedCommand[CVC4::Command*& cmd]
+// Separate this into its own rule (can be invoked by set-info or meta-info)
+metaInfoInternal[CVC4::Command*& cmd]
 @declarations {
-  std::vector<CVC4::Datatype> dts;
-  Type t;
-  Expr e, e2;
+  std::string name;
   SExpr sexpr;
+}
+  : KEYWORD symbolicExpr[sexpr]
+    { name = AntlrInput::tokenText($KEYWORD);
+      if(name == ":cvc4-logic" || name == ":cvc4_logic") {
+        PARSER_STATE->setLogic(sexpr.getValue());
+      } else if(name == ":smt-lib-version") {
+        // if we don't recognize the revision name, just keep the current mode
+        if( (sexpr.isRational() && sexpr.getRationalValue() == Rational(2)) ||
+            sexpr.getValue() == "2" ||
+            sexpr.getValue() == "2.0" ) {
+          PARSER_STATE->setLanguage(language::input::LANG_SMTLIB_V2_0);
+        } else if( (sexpr.isRational() && sexpr.getRationalValue() == Rational(5, 2)) ||
+                   sexpr.getValue() == "2.5" ) {
+          PARSER_STATE->setLanguage(language::input::LANG_SMTLIB_V2_5);
+        }
+      }
+      PARSER_STATE->setInfo(name.c_str() + 1, sexpr);
+      cmd = new SetInfoCommand(name.c_str() + 1, sexpr);
+    }
+  ;
+
+smt25Command[CVC4::Command*& cmd]
+@declarations {
   std::string name;
-  std::vector<std::string> names;
-  std::vector<Expr> terms;
-  std::vector<Type> sorts;
+  Expr expr, expr2;
   std::vector<std::pair<std::string, Type> > sortedVarNames;
+  SExpr sexpr;
+  Type t;
 }
-    /* Extended SMT-LIB set of commands syntax, not permitted in
-     * --smtlib2 compliance mode. */
-  : DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
-  | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd]
-  | /* get model */
-    GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    /* meta-info */
+  : META_INFO_TOK metaInfoInternal[cmd]
+
+    /* declare-const */
+  | DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+    { PARSER_STATE->checkUserSymbol(name); }
+    sortSymbol[t,CHECK_DECLARED]
+    { Expr c = PARSER_STATE->mkVar(name, t);
+      $cmd = new DeclareFunctionCommand(name, c, t); }
+
+    /* get model */
+  | GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     { cmd = new GetModelCommand(); }
+
+    /* echo */
   | ECHO_TOK
     ( simpleSymbolicExpr[sexpr]
       { std::stringstream ss;
@@ -491,17 +533,77 @@ extendedCommand[CVC4::Command*& cmd]
       }
     | { cmd = new EchoCommand(); }
     )
+
+    /* reset: reset everything, returning solver to initial state.
+     * Logic and options must be set again. */
+  | RESET_TOK
+    { cmd = new ResetCommand();
+      PARSER_STATE->reset();
+    }
+    /* reset-assertions: reset assertions, assertion stack, declarations,
+     * etc., but the logic and options remain as they were. */
+  | RESET_ASSERTIONS_TOK
+    { cmd = new ResetAssertionsCommand();
+      PARSER_STATE->resetAssertions();
+    }
+
+  | /* recursive function definition */
+    DEFINE_FUN_REC_TOK { PARSER_STATE->checkThatLogicIsSet(); } LPAREN_TOK
+    { PARSER_STATE->pushScope(true); }
+    ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+      { PARSER_STATE->checkUserSymbol(name); }
+      LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
+      sortSymbol[t,CHECK_DECLARED]
+      { /* add variables to parser state before parsing term */
+        Debug("parser") << "define fun rec: '" << name << "'" << std::endl;
+          if( sortedVarNames.size() > 0 ) {
+          std::vector<CVC4::Type> sorts;
+          sorts.reserve(sortedVarNames.size());
+          for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
+                sortedVarNames.begin(), iend = sortedVarNames.end();
+              i != iend;
+              ++i) {
+            sorts.push_back((*i).second);
+          }
+          t = EXPR_MANAGER->mkFunctionType(sorts, t);
+        }
+        PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED);
+        PARSER_STATE->pushScope(true);
+        for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
+              sortedVarNames.begin(), iend = sortedVarNames.end();
+            i != iend;
+            ++i) {
+          PARSER_STATE->mkBoundVar((*i).first, (*i).second);
+        }
+      }
+      term[expr, expr2]
+      { PARSER_STATE->popScope(); }
+      RPAREN_TOK )+ RPAREN_TOK
+      { PARSER_STATE->popScope(); }
+
+  // CHECK_SAT_ASSUMING still being discussed
+  // GET_UNSAT_ASSUMPTIONS
+  ;
+
+extendedCommand[CVC4::Command*& cmd]
+@declarations {
+  std::vector<CVC4::Datatype> dts;
+  Expr e, e2;
+  Type t;
+  std::string name;
+  std::vector<std::string> names;
+  std::vector<Expr> terms;
+  std::vector<Type> sorts;
+  std::vector<std::pair<std::string, Type> > sortedVarNames;
+}
+    /* Extended SMT-LIB set of commands syntax, not permitted in
+     * --smtlib2 compliance mode. */
+  : DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
+  | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd]
   | rewriterulesCommand[cmd]
 
     /* Support some of Z3's extended SMT-LIB commands */
 
-  | DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
-    { PARSER_STATE->checkUserSymbol(name); }
-    sortSymbol[t,CHECK_DECLARED]
-    { Expr c = PARSER_STATE->mkVar(name, t);
-      $cmd = new DeclareFunctionCommand(name, c, t); }
-      
   | DECLARE_SORTS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF) &&
          !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) &&
@@ -799,11 +901,11 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
 //	}
   | symbol[s,CHECK_NONE,SYM_SORT]
     { sexpr = SExpr(SExpr::Keyword(s)); }
-  | tok=(ASSERT_TOK | CHECKSAT_TOK | DECLARE_FUN_TOK | DECLARE_SORT_TOK | DEFINE_FUN_TOK | DEFINE_SORT_TOK | GET_VALUE_TOK | GET_ASSIGNMENT_TOK | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_CORE_TOK | EXIT_TOK | SET_LOGIC_TOK | SET_INFO_TOK | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | REWRITE_RULE_TOK | REDUCTION_RULE_TOK | PROPAGATION_RULE_TOK | SIMPLIFY_TOK)
+  | tok=(ASSERT_TOK | CHECKSAT_TOK | DECLARE_FUN_TOK | DECLARE_SORT_TOK | DEFINE_FUN_TOK | DEFINE_FUN_REC_TOK | DEFINE_SORT_TOK | GET_VALUE_TOK | GET_ASSIGNMENT_TOK | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_CORE_TOK | EXIT_TOK | RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | REWRITE_RULE_TOK | REDUCTION_RULE_TOK | PROPAGATION_RULE_TOK | SIMPLIFY_TOK)
     { sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); }
   | builtinOp[k]
     { std::stringstream ss;
-      ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2) << EXPR_MANAGER->mkConst(k);
+      ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2_5) << EXPR_MANAGER->mkConst(k);
       sexpr = SExpr(ss.str());
     }
   ;
@@ -1328,15 +1430,15 @@ termList[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr]
  * Matches a string, and strips off the quotes.
  */
 str[std::string& s, bool fsmtlib]
-  : STRING_LITERAL
-    { s = AntlrInput::tokenText($STRING_LITERAL);
+  : STRING_LITERAL_2_0
+    { s = AntlrInput::tokenText($STRING_LITERAL_2_0);
       /* strip off the quotes */
       s = s.substr(1, s.size() - 2);
-	  for(size_t i=0; i<s.size(); i++) {
-		if((unsigned)s[i] > 127) {
-			PARSER_STATE->parseError("Extended characters are not part of SMT-LIB, and they must be encoded as esacped sequences");
-		}
-	  }
+      for(size_t i=0; i<s.size(); i++) {
+        if((unsigned)s[i] > 127) {
+          PARSER_STATE->parseError("Extended characters are not part of SMT-LIB, and they must be encoded as esacped sequences");
+        }
+      }
       if(fsmtlib) {
         /* handle SMT-LIB standard escapes '\\' and '\"' */
         char* p_orig = strdup(s.c_str());
@@ -1360,6 +1462,29 @@ str[std::string& s, bool fsmtlib]
         free(p_orig);
       }
     }
+  | STRING_LITERAL_2_5
+    { s = AntlrInput::tokenText($STRING_LITERAL_2_5);
+      /* strip off the quotes */
+      s = s.substr(1, s.size() - 2);
+      for(size_t i=0; i<s.size(); i++) {
+        if((unsigned)s[i] > 127) {
+          PARSER_STATE->parseError("Extended characters are not part of SMT-LIB, and they must be encoded as esacped sequences");
+        }
+      }
+      // In the 2.5 version, always handle escapes (regardless of fsmtlib flag).
+      char* p_orig = strdup(s.c_str());
+      char *p = p_orig, *q = p_orig;
+      while(*q != '\0') {
+        if(*q == '"') {
+          ++q;
+          assert(*q == '"');
+        }
+        *p++ = *q++;
+      }
+      *p = '\0';
+      s = p_orig;
+      free(p_orig);
+    }
   ;
 
 /**
@@ -1718,6 +1843,7 @@ CHECKSAT_TOK : 'check-sat';
 DECLARE_FUN_TOK : 'declare-fun';
 DECLARE_SORT_TOK : 'declare-sort';
 DEFINE_FUN_TOK : 'define-fun';
+DEFINE_FUN_REC_TOK : 'define-fun-rec';
 DEFINE_SORT_TOK : 'define-sort';
 GET_VALUE_TOK : 'get-value';
 GET_ASSIGNMENT_TOK : 'get-assignment';
@@ -1725,6 +1851,8 @@ GET_ASSERTIONS_TOK : 'get-assertions';
 GET_PROOF_TOK : 'get-proof';
 GET_UNSAT_CORE_TOK : 'get-unsat-core';
 EXIT_TOK : 'exit';
+RESET_TOK : 'reset';
+RESET_ASSERTIONS_TOK : 'reset-assertions';
 ITE_TOK : 'ite';
 LET_TOK : 'let';
 ATTRIBUTE_TOK : '!';
@@ -1733,6 +1861,7 @@ RPAREN_TOK : ')';
 INDEX_TOK : '_';
 SET_LOGIC_TOK : 'set-logic';
 SET_INFO_TOK : 'set-info';
+META_INFO_TOK : 'meta-info';
 GET_INFO_TOK : 'get-info';
 SET_OPTION_TOK : 'set-option';
 GET_OPTION_TOK : 'get-option';
@@ -1960,14 +2089,28 @@ BINARY_LITERAL
   ;
 
 /**
- * Matches a double quoted string literal.  Escaping is supported, and
- * escape character '\' has to be escaped.
+ * Matches a double-quoted string literal from SMT-LIB 2.0.
+ * Escaping is supported, and * escape character '\' has to be escaped.
+ *
+ * You shouldn't generally use this in parser rules, as the quotes
+ * will be part of the token text.  Use the str[] parser rule instead.
+ */
+STRING_LITERAL_2_0
+  : { PARSER_STATE->v2_0() }?=>
+    '"' ('\\' . | ~('\\' | '"'))* '"'
+  ;
+
+/**
+ * Matches a double-quoted string literal from SMT-LIB 2.5.
+ * You escape a double-quote inside the string with "", e.g.,
+ * "This is a string literal with "" a single, embedded double quote."
  *
  * You shouldn't generally use this in parser rules, as the quotes
  * will be part of the token text.  Use the str[] parser rule instead.
  */
-STRING_LITERAL
-  : '"' ('\\' . | ~('\\' | '"'))* '"'
+STRING_LITERAL_2_5
+  : { PARSER_STATE->v2_5() }?=>
+    '"' (~('"') | '""')* '"'
   ;
 
 /**
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 21b6a1e5b..62814ca25 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -233,6 +233,24 @@ bool Smt2::logicIsSet() {
   return d_logicSet;
 }
 
+void Smt2::reset() {
+  d_logicSet = false;
+  d_logic = LogicInfo();
+  operatorKindMap.clear();
+  d_lastNamedTerm = std::pair<Expr, std::string>();
+  d_unsatCoreNames = std::stack< std::map<Expr, std::string> >();
+  this->Parser::reset();
+
+  d_unsatCoreNames.push(std::map<Expr, std::string>());
+  if( !strictModeEnabled() ) {
+    addTheory(Smt2::THEORY_CORE);
+  }
+}
+
+void Smt2::resetAssertions() {
+  this->Parser::reset();
+}
+
 void Smt2::setLogic(const std::string& name) {
   d_logicSet = true;
   if(logicIsForced()) {
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 290bbc975..8c23c8657 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -23,6 +23,7 @@
 #include "parser/smt1/smt1.h"
 #include "theory/logic_info.h"
 #include "util/abstract_value.h"
+#include "parser/smt2/smt2_input.h"
 
 #include <string>
 #include <sstream>
@@ -82,6 +83,10 @@ public:
 
   bool logicIsSet();
 
+  void reset();
+
+  void resetAssertions();
+
   /**
    * Sets the logic for the current benchmark. Declares any logic and
    * theory symbols.
@@ -95,6 +100,17 @@ public:
    */
   const LogicInfo& getLogic() const { return d_logic; }
 
+  bool v2_0() const {
+    return getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_0;
+  }
+  bool v2_5() const {
+    return getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_5;
+  }
+
+  void setLanguage(InputLanguage lang) {
+    ((Smt2Input*) getInput())->setLanguage(lang);
+  }
+
   void setInfo(const std::string& flag, const SExpr& sexpr);
 
   void setOption(const std::string& flag, const SExpr& sexpr);
diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index c1e177dc4..22c2fd9a7 100644
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -29,8 +29,9 @@ namespace CVC4 {
 namespace parser {
 
 /* Use lookahead=2 */
-Smt2Input::Smt2Input(AntlrInputStream& inputStream) :
+Smt2Input::Smt2Input(AntlrInputStream& inputStream, InputLanguage lang) :
   AntlrInput(inputStream, 2) {
+
   pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
   assert( input != NULL );
 
@@ -50,14 +51,21 @@ Smt2Input::Smt2Input(AntlrInputStream& inputStream) :
   }
 
   setAntlr3Parser(d_pSmt2Parser->pParser);
-}
 
+  setLanguage(lang);
+}
 
 Smt2Input::~Smt2Input() {
   d_pSmt2Lexer->free(d_pSmt2Lexer);
   d_pSmt2Parser->free(d_pSmt2Parser);
 }
 
+void Smt2Input::setLanguage(InputLanguage lang) {
+  CheckArgument(lang == language::input::LANG_SMTLIB_V2_0 ||
+                lang == language::input::LANG_SMTLIB_V2_5, lang);
+  d_lang = lang;
+}
+
 Command* Smt2Input::parseCommand() {
   return d_pSmt2Parser->parseCommand(d_pSmt2Parser);
 }
diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h
index b2244db4d..c6a94f07a 100644
--- a/src/parser/smt2/smt2_input.h
+++ b/src/parser/smt2/smt2_input.h
@@ -44,6 +44,9 @@ class Smt2Input : public AntlrInput {
   /** The ANTLR3 SMT2 parser for the input. */
   pSmt2Parser d_pSmt2Parser;
 
+  /** Which (variant of the) input language we're using */
+  InputLanguage d_lang;
+
   /**
    * Initialize the class. Called from the constructors once the input
    * stream is initialized.
@@ -57,16 +60,20 @@ public:
    *
    * @param inputStream the input stream to use
    */
-  Smt2Input(AntlrInputStream& inputStream);
+  Smt2Input(AntlrInputStream& inputStream,
+            InputLanguage lang = language::input::LANG_SMTLIB_V2_5);
 
   /** Destructor. Frees the lexer and the parser. */
   virtual ~Smt2Input();
 
   /** Get the language that this Input is reading. */
   InputLanguage getLanguage() const throw() {
-    return language::input::LANG_SMTLIB_V2;
+    return d_lang;
   }
 
+  /** Set the language that this Input is reading. */
+  void setLanguage(InputLanguage);
+
 protected:
 
   /**
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 220916a1a..94ca46257 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -141,6 +141,7 @@ void AstPrinter::toStream(std::ostream& out, const Command* c,
      tryToStream<CheckSatCommand>(out, c) ||
      tryToStream<QueryCommand>(out, c) ||
      tryToStream<ResetCommand>(out, c) ||
+     tryToStream<ResetAssertionsCommand>(out, c) ||
      tryToStream<QuitCommand>(out, c) ||
      tryToStream<DeclarationSequence>(out, c) ||
      tryToStream<CommandSequence>(out, c) ||
@@ -229,6 +230,10 @@ static void toStream(std::ostream& out, const ResetCommand* c) throw() {
   out << "Reset()";
 }
 
+static void toStream(std::ostream& out, const ResetAssertionsCommand* c) throw() {
+  out << "ResetAssertions()";
+}
+
 static void toStream(std::ostream& out, const QuitCommand* c) throw() {
   out << "Quit()";
 }
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 48f1aadec..f8df9d906 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -860,6 +860,7 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c,
      tryToStream<CheckSatCommand>(out, c, d_cvc3Mode) ||
      tryToStream<QueryCommand>(out, c, d_cvc3Mode) ||
      tryToStream<ResetCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<ResetAssertionsCommand>(out, c, d_cvc3Mode) ||
      tryToStream<QuitCommand>(out, c, d_cvc3Mode) ||
      tryToStream<DeclarationSequence>(out, c, d_cvc3Mode) ||
      tryToStream<CommandSequence>(out, c, d_cvc3Mode) ||
@@ -1051,6 +1052,10 @@ static void toStream(std::ostream& out, const ResetCommand* c, bool cvc3Mode) th
   out << "RESET;";
 }
 
+static void toStream(std::ostream& out, const ResetAssertionsCommand* c, bool cvc3Mode) throw() {
+  out << "RESET ASSERTIONS;";
+}
+
 static void toStream(std::ostream& out, const QuitCommand* c, bool cvc3Mode) throw() {
   //out << "EXIT;";
 }
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index dd2e180e1..a8e2534dc 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -40,7 +40,10 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() {
   case LANG_SMTLIB_V1: // TODO the printer
     return new printer::smt1::Smt1Printer();
 
-  case LANG_SMTLIB_V2:
+  case LANG_SMTLIB_V2_0:
+    return new printer::smt2::Smt2Printer(printer::smt2::smt2_0_variant);
+
+  case LANG_SMTLIB_V2_5:
     return new printer::smt2::Smt2Printer();
 
   case LANG_TPTP:
diff --git a/src/printer/smt1/smt1_printer.cpp b/src/printer/smt1/smt1_printer.cpp
index 474fe58dc..05714fbce 100644
--- a/src/printer/smt1/smt1_printer.cpp
+++ b/src/printer/smt1/smt1_printer.cpp
@@ -33,24 +33,24 @@ namespace smt1 {
 
 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);
+  n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
 }/* Smt1Printer::toStream() */
 
 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);
+  c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
 }/* Smt1Printer::toStream() */
 
 void Smt1Printer::toStream(std::ostream& out, const CommandStatus* s) const throw() {
-  s->toStream(out, language::output::LANG_SMTLIB_V2);
+  s->toStream(out, language::output::LANG_SMTLIB_V2_5);
 }/* Smt1Printer::toStream() */
 
 void Smt1Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
-  Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr);
+  Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, sexpr);
 }/* Smt1Printer::toStream() */
 
 void Smt1Printer::toStream(std::ostream& out, const Model& m) const throw() {
-  Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, m);
+  Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, m);
 }
 
 void Smt1Printer::toStream(std::ostream& out, const Model& m, const Command* c) const throw() {
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 5dc5cb7ee..88bcce5ae 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -125,7 +125,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     if(types) {
       // print the whole type, but not *its* type
       out << ":";
-      n.getType().toStream(out, language::output::LANG_SMTLIB_V2);
+      n.getType().toStream(out, language::output::LANG_SMTLIB_V2_5);
     }
 
     return;
@@ -192,6 +192,27 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       break;
     }
 
+    case kind::CONST_STRING: {
+      const String& s = n.getConst<String>();
+      out << '"';
+      for(size_t i = 0; i < s.size(); ++i) {
+        char c = String::convertUnsignedIntToChar(s[i]);
+        if(c == '"') {
+          if(d_variant == z3str_variant || d_variant == smt2_0_variant) {
+            out << "\\\"";
+          } else {
+            out << "\"\"";
+          }
+        } else if(c == '\\' && (d_variant == z3str_variant || d_variant == smt2_0_variant)) {
+          out << "\\\\";
+        } else {
+          out << c;
+        }
+      }
+      out << '"';
+      break;
+    }
+
     case kind::STORE_ALL: {
       ArrayStoreAll asa = n.getConst<ArrayStoreAll>();
       out << "((as const " << asa.getType() << ") " << asa.getExpr() << ")";
@@ -483,7 +504,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       out << (*i).getType();
       // The following code do stange things
       // (*i).getType().toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
-      //                         false, language::output::LANG_SMTLIB_V2);
+      //                         false, language::output::LANG_SMTLIB_V2_5);
       out << ')';
       if(++i != iend) {
         out << ' ';
@@ -699,6 +720,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c,
      tryToStream<CheckSatCommand>(out, c) ||
      tryToStream<QueryCommand>(out, c) ||
      tryToStream<ResetCommand>(out, c) ||
+     tryToStream<ResetAssertionsCommand>(out, c) ||
      tryToStream<QuitCommand>(out, c) ||
      tryToStream<DeclarationSequence>(out, c) ||
      tryToStream<CommandSequence>(out, c) ||
@@ -714,16 +736,16 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c,
      tryToStream<GetAssertionsCommand>(out, c) ||
      tryToStream<GetProofCommand>(out, c) ||
      tryToStream<GetUnsatCoreCommand>(out, c) ||
-     tryToStream<SetBenchmarkStatusCommand>(out, c) ||
+     tryToStream<SetBenchmarkStatusCommand>(out, c, d_variant) ||
      tryToStream<SetBenchmarkLogicCommand>(out, c, d_variant) ||
-     tryToStream<SetInfoCommand>(out, c) ||
+     tryToStream<SetInfoCommand>(out, c, d_variant) ||
      tryToStream<GetInfoCommand>(out, c) ||
      tryToStream<SetOptionCommand>(out, c) ||
      tryToStream<GetOptionCommand>(out, c) ||
      tryToStream<DatatypeDeclarationCommand>(out, c) ||
-     tryToStream<CommentCommand>(out, c) ||
+     tryToStream<CommentCommand>(out, c, d_variant) ||
      tryToStream<EmptyCommand>(out, c) ||
-     tryToStream<EchoCommand>(out, c)) {
+     tryToStream<EchoCommand>(out, c, d_variant)) {
     return;
   }
 
@@ -733,7 +755,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c,
 }/* Smt2Printer::toStream(Command*) */
 
 static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() {
-  Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr);
+  Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, sexpr);
 }
 
 // SMT-LIB quoting for symbols
@@ -753,7 +775,7 @@ static std::string quoteSymbol(std::string s) {
 
 static std::string quoteSymbol(TNode n) {
   std::stringstream ss;
-  ss << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
+  ss << Expr::setlanguage(language::output::LANG_SMTLIB_V2_5);
   return quoteSymbol(ss.str());
 }
 
@@ -766,13 +788,13 @@ void Smt2Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw()
 }
 
 template <class T>
-static bool tryToStream(std::ostream& out, const CommandStatus* s) throw();
+static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v) throw();
 
 void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const throw() {
 
-  if(tryToStream<CommandSuccess>(out, s) ||
-     tryToStream<CommandFailure>(out, s) ||
-     tryToStream<CommandUnsupported>(out, s)) {
+  if(tryToStream<CommandSuccess>(out, s, d_variant) ||
+     tryToStream<CommandFailure>(out, s, d_variant) ||
+     tryToStream<CommandUnsupported>(out, s, d_variant)) {
     return;
   }
 
@@ -944,6 +966,10 @@ static void toStream(std::ostream& out, const ResetCommand* c) throw() {
   out << "(reset)";
 }
 
+static void toStream(std::ostream& out, const ResetAssertionsCommand* c) throw() {
+  out << "(reset-assertions)";
+}
+
 static void toStream(std::ostream& out, const QuitCommand* c) throw() {
   out << "(exit)";
 }
@@ -1065,8 +1091,12 @@ static void toStream(std::ostream& out, const GetUnsatCoreCommand* c) throw() {
   out << "(get-unsat-core)";
 }
 
-static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() {
-  out << "(set-info :status " << c->getStatus() << ")";
+static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c, Variant v) throw() {
+  if(v == z3str_variant || v == smt2_0_variant) {
+    out << "(set-info :status " << c->getStatus() << ")";
+  } else {
+    out << "(meta-info :status " << c->getStatus() << ")";
+  }
 }
 
 static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c, Variant v) throw() {
@@ -1078,8 +1108,12 @@ static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c, Varia
   }
 }
 
-static void toStream(std::ostream& out, const SetInfoCommand* c) throw() {
-  out << "(set-info :" << c->getFlag() << " ";
+static void toStream(std::ostream& out, const SetInfoCommand* c, Variant v) throw() {
+  if(v == z3str_variant || v == smt2_0_variant) {
+    out << "(set-info :" << c->getFlag() << " ";
+  } else {
+    out << "(meta-info :" << c->getFlag() << " ";
+  }
   toStream(out, c->getSExpr());
   out << ")";
 }
@@ -1126,11 +1160,11 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) thr
   out << "))";
 }
 
-static void toStream(std::ostream& out, const CommentCommand* c) throw() {
+static void toStream(std::ostream& out, const CommentCommand* c, Variant v) throw() {
   string s = c->getComment();
   size_t pos = 0;
   while((pos = s.find_first_of('"', pos)) != string::npos) {
-    s.replace(pos, 1, "\\\"");
+    s.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\"");
     pos += 2;
   }
   out << "(set-info :notes \"" << s << "\")";
@@ -1139,8 +1173,15 @@ static void toStream(std::ostream& out, const CommentCommand* c) throw() {
 static void toStream(std::ostream& out, const EmptyCommand* c) throw() {
 }
 
-static void toStream(std::ostream& out, const EchoCommand* c) throw() {
-  out << "(echo \"" << c->getOutput() << "\")";
+static void toStream(std::ostream& out, const EchoCommand* c, Variant v) throw() {
+  std::string s = c->getOutput();
+  // escape all double-quotes
+  size_t pos = 0;
+  while((pos = s.find('"', pos)) != string::npos) {
+    s.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\"");
+    pos += 2;
+  }
+  out << "(echo \"" << s << "\")";
 }
 
 template <class T>
@@ -1161,13 +1202,13 @@ static bool tryToStream(std::ostream& out, const Command* c, Variant v) throw()
   return false;
 }
 
-static void toStream(std::ostream& out, const CommandSuccess* s) throw() {
+static void toStream(std::ostream& out, const CommandSuccess* s, Variant v) throw() {
   if(Command::printsuccess::getPrintSuccess(out)) {
     out << "success" << endl;
   }
 }
 
-static void toStream(std::ostream& out, const CommandUnsupported* s) throw() {
+static void toStream(std::ostream& out, const CommandUnsupported* s, Variant v) throw() {
 #ifdef CVC4_COMPETITION_MODE
   // if in competition mode, lie and say we're ok
   // (we have nothing to lose by saying success, and everything to lose
@@ -1178,21 +1219,21 @@ static void toStream(std::ostream& out, const CommandUnsupported* s) throw() {
 #endif /* CVC4_COMPETITION_MODE */
 }
 
-static void toStream(std::ostream& out, const CommandFailure* s) throw() {
+static void toStream(std::ostream& out, const CommandFailure* s, Variant v) throw() {
   string message = s->getMessage();
   // escape all double-quotes
   size_t pos = 0;
   while((pos = message.find('"', pos)) != string::npos) {
-    message = message.replace(pos, 1, "\\\"");
+    message.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\"");
     pos += 2;
   }
   out << "(error \"" << message << "\")" << endl;
 }
 
 template <class T>
-static bool tryToStream(std::ostream& out, const CommandStatus* s) throw() {
+static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v) throw() {
   if(typeid(*s) == typeid(T)) {
-    toStream(out, dynamic_cast<const T*>(s));
+    toStream(out, dynamic_cast<const T*>(s), v);
     return true;
   }
   return false;
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index dbbc67fc2..4455a053c 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -29,7 +29,8 @@ namespace smt2 {
 
 enum Variant {
   no_variant,
-  z3str_variant
+  smt2_0_variant, // old-style 2.0 syntax, when it makes a difference
+  z3str_variant // old-style 2.0 and also z3str syntax
 };/* enum Variant */
 
 class Smt2Printer : public CVC4::Printer {
diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp
index cce48ae47..3c46a5849 100644
--- a/src/printer/tptp/tptp_printer.cpp
+++ b/src/printer/tptp/tptp_printer.cpp
@@ -33,26 +33,26 @@ namespace tptp {
 
 void TptpPrinter::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);
+  n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
 }/* TptpPrinter::toStream() */
 
 void TptpPrinter::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);
+  c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
 }/* TptpPrinter::toStream() */
 
 void TptpPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() {
-  s->toStream(out, language::output::LANG_SMTLIB_V2);
+  s->toStream(out, language::output::LANG_SMTLIB_V2_5);
 }/* TptpPrinter::toStream() */
 
 void TptpPrinter::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
-  Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr);
+  Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, sexpr);
 }/* TptpPrinter::toStream() */
 
 void TptpPrinter::toStream(std::ostream& out, const Model& m) const throw() {
   out << "% SZS output start FiniteModel for " << m.getInputName() << endl;
   for(size_t i = 0; i < m.getNumCommands(); ++i) {
-    this->Printer::toStreamUsing(language::output::LANG_SMTLIB_V2, out, m, m.getCommand(i));
+    this->Printer::toStreamUsing(language::output::LANG_SMTLIB_V2_5, out, m, m.getCommand(i));
   }
   out << "% SZS output end FiniteModel for " << m.getInputName() << endl;
 }
diff --git a/src/smt/options b/src/smt/options
index 3ee3dbecb..0dc416474 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -25,7 +25,7 @@ option expandDefinitions expand-definitions bool :default false
  always expand symbol definitions in output
 common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
  support the get-value and get-model commands
-option checkModels check-models --check-models bool :link --produce-models --interactive :link-smt produce-models :link-smt interactive-mode :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+option checkModels check-models --check-models bool :link --produce-models --produce-assertions :link-smt produce-models :link-smt produce-assertions :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions
 option dumpModels --dump-models bool :default false :link --produce-models
  output models after every SAT/INVALID/UNKNOWN response
@@ -45,10 +45,10 @@ option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-uns
 option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  support the get-assignment command
 
-# This could go in src/main/options, but by SMT-LIBv2 spec, "interactive"
-# is a mode in which the assertion list must be kept.  So it belongs here.
-common-option interactive interactive-mode --interactive bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" :read-write
- force interactive mode
+undocumented-option interactiveMode interactive-mode bool :predicate CVC4::smt::beforeSearch CVC4::smt::setProduceAssertions :predicate-include "smt/options_handlers.h" :read-write
+ deprecated name for produce-assertions
+common-option produceAssertions produce-assertions --produce-assertions bool :predicate CVC4::smt::beforeSearch CVC4::smt::setProduceAssertions :predicate-include "smt/options_handlers.h" :read-write
+ keep an assertions list (enables get-assertions command)
 
 option doITESimp --ite-simp bool :read-write
  turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)
@@ -93,7 +93,7 @@ common-option perCallMillisecondLimit  tlimit-per --tlimit-per=MS "unsigned long
  enable time limiting per query (give milliseconds)
 common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long"
  enable resource limiting (currently, roughly the number of SAT conflicts)
-common-option perCallResourceLimit rlimit-per --rlimit-per=N "unsigned long"
+common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long"
  enable resource limiting per query
 
 expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index fcd625267..d02b88fd2 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -299,6 +299,11 @@ inline void beforeSearch(std::string option, bool value, SmtEngine* smt) throw(M
   }
 }
 
+inline void setProduceAssertions(std::string option, bool value, SmtEngine* smt) throw() {
+  options::produceAssertions.set(value);
+  options::interactiveMode.set(value);
+}
+
 // ensure we are a proof-enabled build of CVC4
 inline void proofEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) {
 #ifndef CVC4_PROOF
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 19bfe3ca5..d0a920653 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -603,7 +603,9 @@ public:
       val = d_smt.d_nodeManager->mkAbstractValue(n.getType());
       d_abstractValueMap.addSubstitution(val, n);
     }
-    return val;
+    // We are supposed to ascribe types to all abstract values that go out.
+    Node retval = d_smt.d_nodeManager->mkNode(kind::APPLY_TYPE_ASCRIPTION, d_smt.d_nodeManager->mkConst(AscriptionType(n.getType().toType())), val);
+    return retval;
   }
 
   std::hash_map<Node, Node, NodeHashFunction> rewriteApplyToConstCache;
@@ -675,6 +677,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_modelCommands(NULL),
   d_dumpCommands(),
   d_logic(),
+  d_originalOptions(em->getOptions()),
   d_pendingPops(0),
   d_fullyInited(false),
   d_problemExtended(false),
@@ -737,7 +740,7 @@ void SmtEngine::finishInit() {
   // cleanup ordering issue and Nodes/TNodes.  If SAT is popped
   // first, some user-context-dependent TNodes might still exist
   // with rc == 0.
-  if(options::interactive() ||
+  if(options::produceAssertions() ||
      options::incrementalSolving()) {
     // In the case of incremental solving, we appear to need these to
     // ensure the relevant Nodes remain live.
@@ -961,9 +964,9 @@ void SmtEngine::setDefaults() {
   }
 
   if(options::checkModels()) {
-    if(! options::interactive()) {
-      Notice() << "SmtEngine: turning on interactive-mode to support check-models" << endl;
-      setOption("interactive-mode", SExpr("true"));
+    if(! options::produceAssertions()) {
+      Notice() << "SmtEngine: turning on produce-assertions to support check-models" << endl;
+      setOption("produce-assertions", SExpr("true"));
     }
   }
 
@@ -1450,8 +1453,23 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
   } else if(key == "smt-lib-version") {
     if( (value.isInteger() && value.getIntegerValue() == Integer(2)) ||
         (value.isRational() && value.getRationalValue() == Rational(2)) ||
-        (value.getValue() == "2") ) {
+        value.getValue() == "2" ||
+        value.getValue() == "2.0" ) {
       // supported SMT-LIB version
+      if(!options::outputLanguage.wasSetByUser() &&
+         options::outputLanguage() == language::output::LANG_SMTLIB_V2_5) {
+        options::outputLanguage.set(language::output::LANG_SMTLIB_V2_0);
+        *options::out() << Expr::setlanguage(language::output::LANG_SMTLIB_V2_0);
+      }
+      return;
+    } else if( (value.isRational() && value.getRationalValue() == Rational(5, 2)) ||
+               value.getValue() == "2.5" ) {
+      // supported SMT-LIB version
+      if(!options::outputLanguage.wasSetByUser() &&
+         options::outputLanguage() == language::output::LANG_SMTLIB_V2_0) {
+        options::outputLanguage.set(language::output::LANG_SMTLIB_V2_5);
+        *options::out() << Expr::setlanguage(language::output::LANG_SMTLIB_V2_5);
+      }
       return;
     }
     Warning() << "Warning: unsupported smt-lib-version: " << value << endl;
@@ -1530,6 +1548,8 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
       throw ModalException("Can't get-info :reason-unknown when the "
                            "last result wasn't unknown!");
     }
+  } else if(key == "assertion-stack-levels") {
+    return SExpr(d_userLevels.size());
   } else if(key == "all-options") {
     // get the options, like all-statistics
     return Options::current().getOptions();
@@ -3660,6 +3680,7 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin
 
   if(options::abstractValues() && resultNode.getType().isArray()) {
     resultNode = d_private->mkAbstractValue(resultNode);
+    Trace("smt") << "--- abstract value >> " << resultNode << endl;
   }
 
   return resultNode.toExpr();
@@ -3824,8 +3845,8 @@ Model* SmtEngine::getModel() throw(ModalException) {
 }
 
 void SmtEngine::checkModel(bool hardFailure) {
-  // --check-model implies --interactive, which enables the assertion list,
-  // so we should be ok.
+  // --check-model implies --produce-assertions, which enables the
+  // assertion list, so we should be ok.
   Assert(d_assertionList != NULL, "don't have an assertion list to check in SmtEngine::checkModel()");
 
   TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime);
@@ -4070,9 +4091,9 @@ vector<Expr> SmtEngine::getAssertions() throw(ModalException) {
     Dump("benchmark") << GetAssertionsCommand();
   }
   Trace("smt") << "SMT getAssertions()" << endl;
-  if(!options::interactive()) {
+  if(!options::produceAssertions()) {
     const char* msg =
-      "Cannot query the current assertion list when not in interactive mode.";
+      "Cannot query the current assertion list when not in produce-assertions mode.";
     throw ModalException(msg);
   }
   Assert(d_assertionList != NULL);
@@ -4196,13 +4217,20 @@ void SmtEngine::reset() throw() {
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << ResetCommand();
   }
+  Options opts = d_originalOptions;
   this->~SmtEngine();
+  NodeManager::fromExprManager(em)->getOptions() = opts;
   new(this) SmtEngine(em);
 }
 
 void SmtEngine::resetAssertions() throw() {
   SmtScope smts(this);
 
+  Trace("smt") << "SMT resetAssertions()" << endl;
+  if(Dump.isOn("benchmark")) {
+    Dump("benchmark") << ResetAssertionsCommand();
+  }
+
   while(!d_userLevels.empty()) {
     pop();
   }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 30f84346a..489d34d79 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -189,6 +189,11 @@ class CVC4_PUBLIC SmtEngine {
    */
   LogicInfo d_logic;
 
+  /**
+   * Keep a copy of the original option settings (for reset()).
+   */
+  Options d_originalOptions;
+
   /**
    * Number of internal pops that have been deferred.
    */
diff --git a/src/util/language.cpp b/src/util/language.cpp
index f19f20c03..ca611f729 100644
--- a/src/util/language.cpp
+++ b/src/util/language.cpp
@@ -22,7 +22,8 @@ namespace language {
 InputLanguage toInputLanguage(OutputLanguage language) {
   switch(language) {
   case output::LANG_SMTLIB_V1:
-  case output::LANG_SMTLIB_V2:
+  case output::LANG_SMTLIB_V2_0:
+  case output::LANG_SMTLIB_V2_5:
   case output::LANG_TPTP:
   case output::LANG_CVC4:
   case output::LANG_Z3STR:
@@ -41,7 +42,8 @@ InputLanguage toInputLanguage(OutputLanguage language) {
 OutputLanguage toOutputLanguage(InputLanguage language) {
   switch(language) {
   case input::LANG_SMTLIB_V1:
-  case input::LANG_SMTLIB_V2:
+  case input::LANG_SMTLIB_V2_0:
+  case input::LANG_SMTLIB_V2_5:
   case input::LANG_TPTP:
   case input::LANG_CVC4:
   case input::LANG_Z3STR:
@@ -75,8 +77,12 @@ OutputLanguage toOutputLanguage(std::string language) {
     return output::LANG_SMTLIB_V1;
   } else if(language == "smtlib" || language == "smt" ||
             language == "smtlib2" || language == "smt2" ||
-            language == "LANG_SMTLIB_V2") {
-    return output::LANG_SMTLIB_V2;
+            language == "smtlib2.0" || language == "smt2.0" ||
+            language == "LANG_SMTLIB_V2_0" || language == "LANG_SMTLIB_V2") {
+    return output::LANG_SMTLIB_V2_0;
+  } else if(language == "smtlib2.5" || language == "smt2.5" ||
+            language == "LANG_SMTLIB_V2_5") {
+    return output::LANG_SMTLIB_V2_5;
   } else if(language == "tptp" || language == "LANG_TPTP") {
     return output::LANG_TPTP;
   } else if(language == "z3str" || language == "z3-str" ||
@@ -101,8 +107,12 @@ InputLanguage toInputLanguage(std::string language) {
     return input::LANG_SMTLIB_V1;
   } else if(language == "smtlib" || language == "smt" ||
             language == "smtlib2" || language == "smt2" ||
-            language == "LANG_SMTLIB_V2") {
-    return input::LANG_SMTLIB_V2;
+            language == "smtlib2.0" || language == "smt2.0" ||
+            language == "LANG_SMTLIB_V2_0" || language == "LANG_SMTLIB_V2") {
+    return input::LANG_SMTLIB_V2_0;
+  } else if(language == "smtlib2.5" || language == "smt2.5" ||
+            language == "LANG_SMTLIB_V2_5") {
+    return input::LANG_SMTLIB_V2_5;
   } else if(language == "tptp" || language == "LANG_TPTP") {
     return input::LANG_TPTP;
   } else if(language == "z3str" || language == "z3-str" ||
diff --git a/src/util/language.h b/src/util/language.h
index be962bf3e..abde0b509 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -45,8 +45,12 @@ enum CVC4_PUBLIC Language {
 
   /** The SMTLIB v1 input language */
   LANG_SMTLIB_V1 = 0,
-  /** The SMTLIB v2 input language */
-  LANG_SMTLIB_V2,
+  /** The SMTLIB v2.0 input language */
+  LANG_SMTLIB_V2_0,
+  /** The SMTLIB v2.5 input language */
+  LANG_SMTLIB_V2_5,
+  /** Backward-compatibility for enumeration naming */
+  LANG_SMTLIB_V2 = LANG_SMTLIB_V2_5,
   /** The TPTP input language */
   LANG_TPTP,
   /** The CVC4 input language */
@@ -70,8 +74,11 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_SMTLIB_V1:
     out << "LANG_SMTLIB_V1";
     break;
-  case LANG_SMTLIB_V2:
-    out << "LANG_SMTLIB_V2";
+  case LANG_SMTLIB_V2_0:
+    out << "LANG_SMTLIB_V2_0";
+    break;
+  case LANG_SMTLIB_V2_5:
+    out << "LANG_SMTLIB_V2_5";
     break;
   case LANG_TPTP:
     out << "LANG_TPTP";
@@ -107,7 +114,11 @@ enum CVC4_PUBLIC Language {
 
   /** The SMTLIB v1 output language */
   LANG_SMTLIB_V1 = input::LANG_SMTLIB_V1,
-  /** The SMTLIB v2 output language */
+  /** The SMTLIB v2.0 output language */
+  LANG_SMTLIB_V2_0 = input::LANG_SMTLIB_V2_0,
+  /** The SMTLIB v2.5 output language */
+  LANG_SMTLIB_V2_5 = input::LANG_SMTLIB_V2_5,
+  /** Backward-compatibility for enumeration naming */
   LANG_SMTLIB_V2 = input::LANG_SMTLIB_V2,
   /** The TPTP output language */
   LANG_TPTP = input::LANG_TPTP,
@@ -134,8 +145,11 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_SMTLIB_V1:
     out << "LANG_SMTLIB_V1";
     break;
-  case LANG_SMTLIB_V2:
-    out << "LANG_SMTLIB_V2";
+  case LANG_SMTLIB_V2_0:
+    out << "LANG_SMTLIB_V2_0";
+    break;
+  case LANG_SMTLIB_V2_5:
+    out << "LANG_SMTLIB_V2_5";
     break;
   case LANG_TPTP:
     out << "LANG_TPTP";
diff --git a/src/util/language.i b/src/util/language.i
index 4cbe01df3..3ffc518ac 100644
--- a/src/util/language.i
+++ b/src/util/language.i
@@ -21,6 +21,8 @@ namespace CVC4 {
 %rename(INPUT_LANG_AUTO) CVC4::language::input::LANG_AUTO;
 %rename(INPUT_LANG_SMTLIB_V1) CVC4::language::input::LANG_SMTLIB_V1;
 %rename(INPUT_LANG_SMTLIB_V2) CVC4::language::input::LANG_SMTLIB_V2;
+%rename(INPUT_LANG_SMTLIB_V2_0) CVC4::language::input::LANG_SMTLIB_V2_0;
+%rename(INPUT_LANG_SMTLIB_V2_5) CVC4::language::input::LANG_SMTLIB_V2_5;
 %rename(INPUT_LANG_TPTP) CVC4::language::input::LANG_TPTP;
 %rename(INPUT_LANG_CVC4) CVC4::language::input::LANG_CVC4;
 %rename(INPUT_LANG_MAX) CVC4::language::input::LANG_MAX;
@@ -29,6 +31,8 @@ namespace CVC4 {
 %rename(OUTPUT_LANG_AUTO) CVC4::language::output::LANG_AUTO;
 %rename(OUTPUT_LANG_SMTLIB_V1) CVC4::language::output::LANG_SMTLIB_V1;
 %rename(OUTPUT_LANG_SMTLIB_V2) CVC4::language::output::LANG_SMTLIB_V2;
+%rename(OUTPUT_LANG_SMTLIB_V2_0) CVC4::language::output::LANG_SMTLIB_V2_0;
+%rename(OUTPUT_LANG_SMTLIB_V2_5) CVC4::language::output::LANG_SMTLIB_V2_5;
 %rename(OUTPUT_LANG_TPTP) CVC4::language::output::LANG_TPTP;
 %rename(OUTPUT_LANG_CVC4) CVC4::language::output::LANG_CVC4;
 %rename(OUTPUT_LANG_AST) CVC4::language::output::LANG_AST;
diff --git a/test/regress/regress0/bug421.smt2 b/test/regress/regress0/bug421.smt2
index 5a5886940..fd7b4a7cc 100644
--- a/test/regress/regress0/bug421.smt2
+++ b/test/regress/regress0/bug421.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --incremental --abstract-values
 ; EXPECT: sat
-; EXPECT: ((a @1) (b @2))
+; EXPECT: ((a (as @1 (Array Int Int))) (b (as @2 (Array Int Int))))
 (set-logic QF_AUFLIA)
 (set-option :produce-models true)
 (declare-fun a () (Array Int Int))
diff --git a/test/regress/regress0/bug421b.smt2 b/test/regress/regress0/bug421b.smt2
index 82f566a64..aed7f7c05 100644
--- a/test/regress/regress0/bug421b.smt2
+++ b/test/regress/regress0/bug421b.smt2
@@ -4,7 +4,7 @@
 ;
 ; COMMAND-LINE: --incremental --abstract-values --check-models
 ; EXPECT: sat
-; EXPECT: ((a @1) (b @2))
+; EXPECT: ((a (as @1 (Array Int Int))) (b (as @2 (Array Int Int))))
 (set-logic QF_AUFLIA)
 (set-option :produce-models true)
 (declare-fun a () (Array Int Int))
diff --git a/test/regress/regress0/bug590.smt2 b/test/regress/regress0/bug590.smt2
index d5bd7fd56..06dc1fe58 100644
--- a/test/regress/regress0/bug590.smt2
+++ b/test/regress/regress0/bug590.smt2
@@ -1,6 +1,7 @@
 (set-logic QF_ALL_SUPPORTED)
 (set-option :strings-exp true)
 (set-option :produce-models true)
+(set-info :smt-lib-version 2.0)
 (set-info :status sat)
 
 (declare-fun text () String)
diff --git a/test/regress/regress0/crash_burn_locusts.smt2 b/test/regress/regress0/crash_burn_locusts.smt2
new file mode 100644
index 000000000..313d6f79c
--- /dev/null
+++ b/test/regress/regress0/crash_burn_locusts.smt2
@@ -0,0 +1,29 @@
+;; This is a nasty parsing test for define-fun-rec
+
+(set-logic UFLIRA)
+(set-info :smt-lib-version 2.5)
+(define-fun-rec (
+   (f ((x Int)) Int 5) ;; ok, f : Int -> Int
+   (g ((x Int)) Int (h 4)) ;;  um, ok, so g : Int -> Int and h : Int -> Int?
+   (h ((x Real)) Int 4)   ;; oops no we were wrong, **CRASH**
+))
+
+(reset)
+
+(set-logic UFLIRA)
+(set-info :smt-lib-version 2.5)
+(define-fun-rec (
+   (f ((x Int)) Int (g (h 4) 5)) ;; ok, f : Int -> Int and g : Int -> X -> Int and h : Int -> X ??!  What the F?! (pun intended)
+   (g ((x Int)) Int 5) ;; wait, now g has wrong arity?!!  **BURN**
+   (h ((x Int)) Int 2)
+))
+
+(reset)
+
+(set-logic UFLIRA)
+(set-info :smt-lib-version 2.5)
+(declare-const g Int 2)
+(define-fun-rec (
+  (f () Int g)  ;; wait, which g does this refer to?!  **LOCUSTS**
+  (g () Int 5)
+))
diff --git a/test/regress/regress0/parser/Makefile.am b/test/regress/regress0/parser/Makefile.am
index 389c80e09..eb27e797b 100644
--- a/test/regress/regress0/parser/Makefile.am
+++ b/test/regress/regress0/parser/Makefile.am
@@ -19,7 +19,9 @@ MAKEFLAGS = -k
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
 TESTS =	\
-	declarefun-emptyset-uf.smt2
+	declarefun-emptyset-uf.smt2 \
+	strings20.smt2 \
+	strings25.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/parser/strings20.smt2 b/test/regress/regress0/parser/strings20.smt2
new file mode 100644
index 000000000..6e9ea4434
--- /dev/null
+++ b/test/regress/regress0/parser/strings20.smt2
@@ -0,0 +1,15 @@
+; EXPECT: sat
+; EXPECT: (model
+; EXPECT: (define-fun s () String "\"")
+; EXPECT: )
+
+(set-logic QF_S)
+(set-info :smt-lib-version 2.0)
+(set-option :produce-models true)
+
+(declare-fun s () String)
+
+(assert (= s "\""))
+
+(check-sat)
+(get-model)
diff --git a/test/regress/regress0/parser/strings25.smt2 b/test/regress/regress0/parser/strings25.smt2
new file mode 100644
index 000000000..90602e67d
--- /dev/null
+++ b/test/regress/regress0/parser/strings25.smt2
@@ -0,0 +1,15 @@
+; EXPECT: sat
+; EXPECT: (model
+; EXPECT: (define-fun s () String """")
+; EXPECT: )
+
+(set-logic QF_S)
+(set-info :smt-lib-version 2.5)
+(set-option :produce-models true)
+
+(declare-fun s () String)
+
+(assert (= s """"))
+
+(check-sat)
+(get-model)
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 233962d72..bd8e9ea93 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -23,6 +23,7 @@ TESTS =	\
   bug001.smt2 \
   cardinality.smt2 \
   escchar.smt2 \
+  escchar_25.smt2 \
   str001.smt2 \
   str002.smt2 \
   str003.smt2 \
diff --git a/test/regress/regress0/strings/escchar.smt2 b/test/regress/regress0/strings/escchar.smt2
index 508d7f3c1..aa2afb7e4 100644
--- a/test/regress/regress0/strings/escchar.smt2
+++ b/test/regress/regress0/strings/escchar.smt2
@@ -1,5 +1,6 @@
 (set-logic QF_S)
 (set-info :status sat)
+(set-info :smt-lib-version 2.0)
 
 (declare-fun x () String)
 (declare-const I Int)
diff --git a/test/regress/regress0/strings/escchar_25.smt2 b/test/regress/regress0/strings/escchar_25.smt2
new file mode 100644
index 000000000..f48995344
--- /dev/null
+++ b/test/regress/regress0/strings/escchar_25.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_S)
+(set-info :status sat)
+(set-info :smt-lib-version 2.5)
+
+(declare-fun x () String)
+(declare-const I Int)
+
+(assert (= x "\0\1\2\3\04\005\x06\7\8\9ABC\\""\t\a\b"))
+(assert (= I (str.len x)))
+
+
+(check-sat)