From 3ea71b4b25739cae6fa432038c0251e75c2f0fdf Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Tue, 14 Jun 2016 12:49:48 +0100
Subject: [PATCH] Fixed SMT2 scanner to allow 0xFF characters.

Thanks to Santiago Zanella-Beguelin for reporting this issue.
---
 src/parsers/smt2/smt2scanner.cpp | 25 +++++++++++++++----------
 src/parsers/smt2/smt2scanner.h   |  1 +
 2 files changed, 16 insertions(+), 10 deletions(-)

diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp
index 156cc2e5d..911f449dc 100644
--- a/src/parsers/smt2/smt2scanner.cpp
+++ b/src/parsers/smt2/smt2scanner.cpp
@@ -23,10 +23,12 @@ namespace smt2 {
 
     void scanner::next() {
         if (m_cache_input)
-            m_cache.push_back(m_curr);
-        SASSERT(m_curr != EOF);
+            m_cache.push_back(m_curr);                
+        SASSERT(!m_at_eof);
         if (m_interactive) {
             m_curr = m_stream.get();
+            if (m_stream.eof())
+                m_at_eof = true;
         }
         else if (m_bpos < m_bend) {
             m_curr = m_buffer[m_bpos];
@@ -37,7 +39,7 @@ namespace smt2 {
             m_bend = static_cast<unsigned>(m_stream.gcount());
             m_bpos = 0;
             if (m_bpos == m_bend) {
-                m_curr = EOF;
+                m_at_eof = true;
             }
             else {
                 m_curr = m_buffer[m_bpos];
@@ -52,7 +54,7 @@ namespace smt2 {
         next();
         while (true) {
             char c = curr();
-            if (c == EOF)
+            if (m_at_eof)
                 return;
             if (c == '\n') {
                 new_line();
@@ -70,7 +72,7 @@ namespace smt2 {
         next();
         while (true) {
             char c = curr();
-            if (c == EOF) {
+            if (m_at_eof) {
                 throw scanner_exception("unexpected end of quoted symbol", m_line, m_spos);
             }
             else if (c == '\n') {
@@ -167,7 +169,7 @@ namespace smt2 {
         m_string.reset();
         while (true) {
             char c = curr();
-            if (c == EOF)
+            if (m_at_eof)
                 throw scanner_exception("unexpected end of string", m_line, m_spos);
             if (c == '\n') {
                 new_line();
@@ -237,10 +239,11 @@ namespace smt2 {
         }
     }
 
-    scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive):
+    scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive) :
         m_interactive(interactive),
         m_spos(0),
         m_curr(0), // avoid Valgrind warning
+        m_at_eof(false),
         m_line(1),
         m_pos(0),
         m_bv_size(UINT_MAX),
@@ -289,9 +292,13 @@ namespace smt2 {
     }
 
     scanner::token scanner::scan() {
-        while (true) {
+        while (true) {            
             signed char c = curr();
             m_pos = m_spos;
+
+            if (m_at_eof)                
+                return EOF_TOKEN;
+
             switch (m_normalized[(unsigned char) c]) {
             case ' ':
                 next();
@@ -327,8 +334,6 @@ namespace smt2 {
                     return read_symbol();
                 else
                     return read_signed_number();
-            case -1:
-                return EOF_TOKEN;
             default: {
                 scanner_exception ex("unexpected character", m_line, m_spos);
                 next();
diff --git a/src/parsers/smt2/smt2scanner.h b/src/parsers/smt2/smt2scanner.h
index 8313c24df..3ad47dfb1 100644
--- a/src/parsers/smt2/smt2scanner.h
+++ b/src/parsers/smt2/smt2scanner.h
@@ -34,6 +34,7 @@ namespace smt2 {
         bool               m_interactive;
         int                m_spos; // position in the current line of the stream
         char               m_curr;  // current char;
+        bool               m_at_eof;
         
         int                m_line;  // line
         int                m_pos;   // start position of the token