From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 19 Jun 2013 15:11:27 +0000 (-0400)
Subject: Fix to the "include" extended feature of the SMT-LIB parser
X-Git-Tag: cvc5-1.0.0~7287^2~94
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=28b20dc558e00d8111a289d31da83270fa581a03;p=cvc5.git

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

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 883f1f12b..91566f5f6 100644
--- 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 373f5b3a4..cb9a13c20 100644
--- 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';