diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index dad485d94..82607452f 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -561,6 +561,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
     zstring s;
     rational pos, len;
 
+    TRACE("seq", tout << mk_pp(a, m()) << " " << mk_pp(b, m()) << " " << mk_pp(c, m()) << "\n";);
     bool constantBase = m_util.str.is_string(a, s);
     bool constantPos = m_autil.is_numeral(b, pos);
     bool constantLen = m_autil.is_numeral(c, len);
@@ -599,6 +600,10 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
         SASSERT(_len > 0);
         expr_ref_vector as(m()), bs(m());
         m_util.str.get_concat(a, as);
+        if (as.empty()) {
+            result = a;
+            return BR_DONE;
+        }
         for (unsigned i = 0; i < as.size() && _len > 0; ++i) {
             if (m_util.str.is_unit(as[i].get())) {
                 if (_pos == 0) {
@@ -613,7 +618,12 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
                 return BR_FAILED;
             }
         }
-        result = m_util.str.mk_concat(bs);
+        if (bs.empty()) {
+            result = m_util.str.mk_empty(m().get_sort(a));
+        }
+        else {
+            result = m_util.str.mk_concat(bs);
+        }
         return BR_DONE;
     }
 
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 106a77c0e..64f9c36fd 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -346,7 +346,8 @@ namespace smt2 {
         // consume garbage
         // return true if managed to recover from the error...
         bool sync_after_error() {
-            while (true) {
+            unsigned num_errors = 0;
+            while (num_errors < 100) {
                 try {
                     while (curr_is_rparen())
                         next();
@@ -374,8 +375,10 @@ namespace smt2 {
                 catch (scanner_exception & ex) {
                     SASSERT(ex.has_pos());
                     error(ex.line(), ex.pos(), ex.msg());
+                    ++num_errors;
                 }
             }
+            return false;
         }
 
         void check_next(scanner::token t, char const * msg) {
@@ -3117,7 +3120,7 @@ namespace smt2 {
 
         bool operator()() {
             m_num_bindings    = 0;
-            bool found_errors = false;
+            unsigned found_errors = 0;
 
             try {
                 scan_core();
@@ -3126,7 +3129,7 @@ namespace smt2 {
                 error(ex.msg());
                 if (!sync_after_error())
                     return false;
-                found_errors = true;
+                found_errors++;
             }
 
             while (true) {
@@ -3138,7 +3141,7 @@ namespace smt2 {
                             parse_cmd();
                             break;
                         case scanner::EOF_TOKEN:
-                            return !found_errors;
+                            return found_errors == 0;
                         default:
                             throw parser_exception("invalid command, '(' expected");
                             break;