diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp
index 9a9e69b67..e1725dada 100644
--- a/src/parsers/smt2/smt2scanner.cpp
+++ b/src/parsers/smt2/smt2scanner.cpp
@@ -64,6 +64,26 @@ namespace smt2 {
             next();
         }
     }
+    
+    void scanner::read_multiline_comment() {
+        SASSERT(curr() == '|');
+        next();
+        while (true) {
+            char c = curr();
+            if (m_at_eof)
+                return;
+            if (c == '\n') {
+                new_line();
+                next();
+                continue;
+            }
+            next();
+            if (c == '|' && curr() == '#') {
+                next();
+                return;
+            }
+        }
+    }
 
     scanner::token scanner::read_quoted_symbol() {
         SASSERT(curr() == '|');
@@ -235,6 +255,10 @@ namespace smt2 {
                 throw scanner_exception("invalid empty bit-vector literal", m_line, m_spos);
             return BV_TOKEN;
         }
+        else if ('|') {
+            read_multiline_comment();
+            return NULL_TOKEN;
+        }
         else {
             throw scanner_exception("invalid bit-vector literal, expecting 'x' or 'b'", m_line, m_spos);
         }
@@ -295,6 +319,8 @@ namespace smt2 {
     scanner::token scanner::scan() {
         while (true) {
             signed char c = curr();
+            token t;
+            
             m_pos = m_spos;
 
             if (m_at_eof)
@@ -329,7 +355,9 @@ namespace smt2 {
             case '0':
                 return read_number();
             case '#':
-                return read_bv_literal();
+                t = read_bv_literal();
+                if (t == NULL_TOKEN) break;
+                return t;
             case '-':
                 if (m_smtlib2_compliant)
                     return read_symbol();
diff --git a/src/parsers/smt2/smt2scanner.h b/src/parsers/smt2/smt2scanner.h
index 5283c57cf..5fad416b0 100644
--- a/src/parsers/smt2/smt2scanner.h
+++ b/src/parsers/smt2/smt2scanner.h
@@ -92,6 +92,7 @@ namespace smt2 {
         token read_symbol();
         token read_quoted_symbol();
         void read_comment();
+        void read_multiline_comment();
         token read_number();
         token read_signed_number();
         token read_string();