diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-07 15:23:36 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-07 15:23:36 -0400 |
| commit | 931b5641dfffcd3779239e014406aa057e21e0f7 (patch) | |
| tree | cc37b63036dc8cd88af2c8cb1ac4511d0befbf17 /src/parser/smt2/Smt2.g | |
| parent | 6a329424666b4c4a6869dd7bcf9e7cfd69a219f5 (diff) | |
Allow disabling include-file feature
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 29bc8d40f..5abaa0163 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -197,7 +197,10 @@ parseCommand returns [CVC4::Command* cmd = NULL] * the RPAREN_TOK is properly eaten and we are in a good state to read * the included file's tokens. */ | LPAREN_TOK INCLUDE_TOK str[name] RPAREN_TOK - { if(PARSER_STATE->strictModeEnabled()) { + { if(!PARSER_STATE->canIncludeFile()) { + PARSER_STATE->parseError("include-file feature was disabled for this run."); + } + if(PARSER_STATE->strictModeEnabled()) { PARSER_STATE->parseError("Extended commands are not permitted while operating in strict compliance mode."); } PARSER_STATE->includeFile(name); |