1 files changed, 2 insertions, 36 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 7ef7edbbe..ea45e2e61 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -480,12 +480,6 @@ command [std::unique_ptr<CVC4::Command>* cmd]
 
     /* 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]
@@ -900,9 +894,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
 }
     /* Extended SMT-LIB set of commands syntax, not permitted in
      * --smtlib2 compliance mode. */
-  : DECLARE_DATATYPES_2_5_TOK datatypes_2_5_DefCommand[false, cmd]
-  | DECLARE_CODATATYPES_2_5_TOK datatypes_2_5_DefCommand[true, cmd]
-  | DECLARE_CODATATYPE_TOK datatypeDefCommand[true, cmd]
+  : DECLARE_CODATATYPE_TOK datatypeDefCommand[true, cmd]
   | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd]
 
     /* Support some of Z3's extended SMT-LIB commands */
@@ -1081,32 +1073,6 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
     )
   ;
 
-
-datatypes_2_5_DefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
-@declarations {
-  std::vector<api::DatatypeDecl> dts;
-  std::string name;
-  std::vector<api::Sort> sorts;
-  std::vector<std::string> dnames;
-  std::vector<unsigned> arities;
-}
-  : { PARSER_STATE->checkThatLogicIsSet();
-    /* open a scope to keep the UnresolvedTypes contained */
-    PARSER_STATE->pushScope(); }
-  LPAREN_TOK /* parametric sorts */
-  ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
-    {
-      sorts.push_back(PARSER_STATE->mkSort(name));
-    }
-  )*
-  RPAREN_TOK
-  LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK
-  { PARSER_STATE->popScope();
-    cmd->reset(new DatatypeDeclarationCommand(
-        PARSER_STATE->bindMutualDatatypeTypes(dts, true)));
-  }
-  ;
-
 datatypeDefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
 @declarations {
   std::vector<api::DatatypeDecl> dts;
@@ -2226,7 +2192,7 @@ GET_PROOF_TOK : 'get-proof';
 GET_UNSAT_ASSUMPTIONS_TOK : 'get-unsat-assumptions';
 GET_UNSAT_CORE_TOK : 'get-unsat-core';
 EXIT_TOK : 'exit';
-RESET_TOK : { PARSER_STATE->v2_5() }? 'reset';
+RESET_TOK : 'reset';
 RESET_ASSERTIONS_TOK : 'reset-assertions';
 LET_TOK : 'let';
 ATTRIBUTE_TOK : '!';