Fix parsing of SMT-LIBv2 |quoted| symbols that span newlines in interactive mode.

Thanks to David Cok for raising this issue.

diff --git a/src/parser/parser.h b/src/parser/parser.h
index d13fbf2d6a719eb7bf9cd0cb5ffd89eb21e1d968..0761b4cda30fe8bb5b1830a448c3baf7ba1448db 100644 (file)
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -462,6 +462,11 @@ public:
     d_input->parseError(msg);
   }
 
+  /** Unexpectedly encountered an EOF */
+  inline void unexpectedEOF(const std::string& msg) throw(ParserException) {
+    d_input->parseError(msg, true);
+  }
+
   /**
    * If we are parsing only, don't raise an exception; if we are not,
    * raise a parse error with the given message.  There is no actual

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 7bbcb85d800bbd9309a928feb5153b306cc30185..29b6e0fbb7d68f62d5e1e5430575a25e8fb4f45a 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1346,6 +1346,8 @@ symbol[std::string& id,
         PARSER_STATE->checkDeclaration(id, check, type);
       }
     }
+  | UNTERMINATED_QUOTED_SYMBOL EOF
+    { PARSER_STATE->unexpectedEOF("unterminated |quoted| symbol"); }
   ;
 
 /**
@@ -1539,6 +1541,9 @@ BVSGE_TOK : 'bvsge';
 QUOTED_SYMBOL
   : '|' ~('|' | '\\')* '|'
   ;
+UNTERMINATED_QUOTED_SYMBOL
+  : '|' ~('|' | '\\')*
+  ;
 
 /**
  * Matches a keyword from the input. A keyword is a simple symbol prefixed