Fix tokenization of "reset" in SMT-LIB v2.0. It's a reserved word only in 2.5.

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index f9b222b2b2534d2c0241725fd9f6971909edc9c0..df71f13c9731081e13caf80b729425ca2fd619f2 100644 (file)
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -187,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_5);
+        opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2_0);
       } 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)) {

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index a8d42a740168485ec93913a89e3a2be18851fa8a..bdad4560610bc571614b92a35dd9b5d7a8b199f2 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1884,7 +1884,7 @@ GET_ASSERTIONS_TOK : 'get-assertions';
 GET_PROOF_TOK : 'get-proof';
 GET_UNSAT_CORE_TOK : 'get-unsat-core';
 EXIT_TOK : 'exit';
-RESET_TOK : 'reset';
+RESET_TOK : { PARSER_STATE->v2_5() }? 'reset';
 RESET_ASSERTIONS_TOK : 'reset-assertions';
 ITE_TOK : 'ite';
 LET_TOK : 'let';