Allow disabling include-file feature

2 files changed, 9 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);
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index be4907e8e..42324fe1e 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -242,6 +242,11 @@ static bool newInputStream(const std::string& filename, pANTLR3_LEXER lexer) {
 }
 
 void Smt2::includeFile(const std::string& filename) {
+  // security for online version
+  if(!canIncludeFile()) {
+    parseError("include-file feature was disabled for this run.");
+  }
+
   // Get the lexer
   AntlrInput* ai = static_cast<AntlrInput*>(getInput());
   pANTLR3_LEXER lexer = ai->getAntlr3Lexer();