From aef543d74c4fb23a86ad2986d67e7fc7f11d1feb Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 17 May 2013 17:04:34 -0400
Subject: [PATCH] Fix parsing of SMT-LIBv2 |quoted| symbols that span newlines
 in interactive mode.

Thanks to David Cok for raising this issue.
---
 src/parser/parser.h    | 5 +++++
 src/parser/smt2/Smt2.g | 5 +++++
 2 files changed, 10 insertions(+)

diff --git a/src/parser/parser.h b/src/parser/parser.h
index d13fbf2d6..0761b4cda 100644
--- 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 7bbcb85d8..29b6e0fbb 100644
--- 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
-- 
2.30.2