Fix to the "include" extended feature of the SMT-LIB parser

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 883f1f12b56e6fad8dd14774cf349584885c8da9..91566f5f626d7beb1720f0fd16f842e20afa5256 100644 (file)
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -258,8 +258,8 @@ public:
 
   bool strictModeEnabled() { return d_strictMode; }
 
-  bool allowIncludeFile() { d_canIncludeFile = true; }
-  bool disallowIncludeFile() { d_canIncludeFile = false; }
+  void allowIncludeFile() { d_canIncludeFile = true; }
+  void disallowIncludeFile() { d_canIncludeFile = false; }
   bool canIncludeFile() const { return d_canIncludeFile; }
 
   /**

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 373f5b3a42383db5b8b94b37a4d4fac89dc6845d..cb9a13c20b4a8af09ebbf5c8d94ab507dc3de416 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1483,7 +1483,7 @@ DECLARE_PREDS_TOK : 'declare-preds';
 DEFINE_TOK : 'define';
 DECLARE_CONST_TOK : 'declare-const';
 SIMPLIFY_TOK : 'simplify';
-INCLUDE_TOK : 'include-file';
+INCLUDE_TOK : 'include';
 
 // attributes
 ATTRIBUTE_PATTERN_TOK : ':pattern';