3 files changed, 34 insertions, 1 deletions
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.
  */