diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp
index 3664ed903..8a0dc1639 100644
--- a/src/parsers/smt2/smt2scanner.cpp
+++ b/src/parsers/smt2/smt2scanner.cpp
@@ -46,7 +46,7 @@ namespace smt2 {
         }
         m_spos++;
     }
-    
+
     void scanner::read_comment() {
         SASSERT(curr() == ';');
         next();
@@ -62,7 +62,7 @@ namespace smt2 {
             next();
         }
     }
-    
+
     scanner::token scanner::read_quoted_symbol() {
         SASSERT(curr() == '|');
         bool escape = false;
@@ -105,7 +105,7 @@ namespace smt2 {
             }
         }
     }
-    
+
     scanner::token scanner::read_symbol() {
         SASSERT(m_normalized[static_cast<unsigned>(curr())] == 'a' || curr() == ':' || curr() == '-');
         m_string.reset();
@@ -113,14 +113,14 @@ namespace smt2 {
         next();
         return read_symbol_core();
     }
-    
+
     scanner::token scanner::read_number() {
         SASSERT('0' <= curr() && curr() <= '9');
         rational q(1);
         m_number = rational(curr() - '0');
         next();
         bool is_float = false;
-        
+
         while (true) {
             char c = curr();
             if ('0' <= c && c <= '9') {
@@ -139,7 +139,7 @@ namespace smt2 {
                 break;
             }
         }
-        if (is_float) 
+        if (is_float)
             m_number /= q;
         TRACE("scanner", tout << "new number: " << m_number << "\n";);
         return is_float ? FLOAT_TOKEN : INT_TOKEN;
@@ -160,14 +160,14 @@ namespace smt2 {
             return read_symbol_core();
         }
     }
-    
+
     scanner::token scanner::read_string() {
         SASSERT(curr() == '\"');
         next();
         m_string.reset();
         while (true) {
             char c = curr();
-            if (c == EOF) 
+            if (c == EOF)
                 throw scanner_exception("unexpected end of string", m_line, m_spos);
             if (c == '\n') {
                 new_line();
@@ -179,11 +179,19 @@ namespace smt2 {
                     return STRING_TOKEN;
                 }
             }
+            else if (c == '\\') {
+                next();
+                c = curr();
+                if (c == EOF)
+                    throw scanner_exception("unexpected end of string", m_line, m_spos);
+                if (c != '\\' && c != '\"')
+                    throw scanner_exception("invalid escape sequence", m_line, m_spos);
+            }
             m_string.push_back(c);
             next();
         }
     }
-    
+
     scanner::token scanner::read_bv_literal() {
         SASSERT(curr() == '#');
         next();
@@ -200,7 +208,7 @@ namespace smt2 {
                 }
                 else if ('a' <= c && c <= 'f') {
                     m_number *= rational(16);
-                    m_number += rational(10 + (c - 'a')); 
+                    m_number += rational(10 + (c - 'a'));
                 }
                 else if ('A' <= c && c <= 'F') {
                     m_number *= rational(16);
@@ -236,9 +244,9 @@ namespace smt2 {
             throw scanner_exception("invalid bit-vector literal, expecting 'x' or 'b'", m_line, m_spos);
         }
     }
-    
+
     scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive):
-        m_interactive(interactive), 
+        m_interactive(interactive),
         m_spos(0),
         m_curr(0), // avoid Valgrind warning
         m_line(1),
@@ -248,7 +256,7 @@ namespace smt2 {
         m_bend(0),
         m_stream(stream),
         m_cache_input(false) {
-        
+
         m_smtlib2_compliant = ctx.params().m_smtlib2_compliant;
 
         for (int i = 0; i < 256; ++i) {
@@ -287,7 +295,7 @@ namespace smt2 {
         m_normalized[static_cast<int>('/')] = 'a';
         next();
     }
-    
+
     scanner::token scanner::scan() {
         while (true) {
             signed char c = curr();