summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-06-19 11:11:27 -0400
committerMorgan Deters <mdeters@cs.nyu.edu>2013-06-19 11:11:27 -0400
commit28b20dc558e00d8111a289d31da83270fa581a03 (patch)
tree3d90d7aa92cb4a92824ee5a8732ec184c44dddf5
parent010ad47b7b3e1909f31525fc45be2c27c1b72e45 (diff)
Fix to the "include" extended feature of the SMT-LIB parser
-rw-r--r--src/parser/parser.h4
-rw-r--r--src/parser/smt2/Smt2.g2
2 files changed, 3 insertions, 3 deletions
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';
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback