From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 12 Nov 2014 13:29:00 +0000 (-0500)
Subject: Fix tokenization of "reset" in SMT-LIB v2.0.  It's a reserved word only in 2.5.
X-Git-Tag: cvc5-1.0.0~6502
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=18b06f0431eefd5006fffc7794852365c48b2bb6;p=cvc5.git

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 f9b222b2b..df71f13c9 100644
--- 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 a8d42a740..bdad45606 100644
--- 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';