diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index 5f2d36279..ceeab30ff 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -238,7 +238,7 @@ format * smt2_pp_environment::pp_float_literal(app * t, bool use_bv_lits, bool u
     string_buffer<> buf;
     VERIFY(get_futil().is_numeral(t, v));
     if (fm.is_nan(v)) {
-        buf << "(_ NaN " << v.get().get_ebits() << " " << v.get().get_sbits() << ")";
+        buf << "(_ NaN " << v.get().get_ebits() << " " << v.get().get_sbits() << ")";        
         return mk_string(m, buf.c_str());
     }
     else if (fm.is_pinf(v)) {
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index f5d76f7e6..3dc76da5e 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -780,13 +780,11 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_
     }
 
     expr* c = nullptr, *t = nullptr, *e = nullptr;
-    if (m().is_ite(arg, c, t, e)) {
-        if ((t->get_ref_count() == 1 && e->get_ref_count() == 1) ||
-            (!m().is_ite(t) && !m().is_ite(e))) {
-            //std::cout << "n-ite\n";
-            result = m().mk_ite(c, m_mk_extract(high, low, t), m_mk_extract(high, low, e));
-            return BR_REWRITE2;
-        }
+    if (m().is_ite(arg, c, t, e) &&
+        (t->get_ref_count() == 1 || !m().is_ite(t)) && 
+        (e->get_ref_count() == 1 || !m().is_ite(e))) {
+        result = m().mk_ite(c, m_mk_extract(high, low, t), m_mk_extract(high, low, e));
+        return BR_REWRITE2;
     }
 
     return BR_FAILED;
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 54d1811e6..9be03ad6e 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2396,7 +2396,6 @@ bool theory_seq::is_var(expr* a) const {
         !m_util.str.is_string(a) &&
         !m_util.str.is_unit(a) &&
         !m_util.str.is_itos(a) && 
-        !m_util.str.is_extract(a) && 
         !m.is_ite(a);
 }
 
@@ -4812,11 +4811,15 @@ void theory_seq::add_extract_axiom(expr* e) {
 void theory_seq::add_tail_axiom(expr* e, expr* s) {
     expr_ref head(m), tail(m);
     mk_decompose(s, head, tail);
-    add_axiom(mk_eq_empty(s), mk_seq_eq(s, mk_concat(head, e)));
+    literal emp = mk_eq_empty(s);
+    add_axiom(emp, mk_seq_eq(s, mk_concat(head, e)));
+    add_axiom(~emp, mk_eq_empty(e));
 }
 
 void theory_seq::add_drop_last_axiom(expr* e, expr* s) {
-    add_axiom(mk_eq_empty(s), mk_seq_eq(s, mk_concat(e, m_util.str.mk_unit(mk_last(s)))));
+    literal emp = mk_eq_empty(s);
+    add_axiom(emp, mk_seq_eq(s, mk_concat(e, m_util.str.mk_unit(mk_last(s)))));
+    add_axiom(~emp, mk_eq_empty(e));
 }
 
 bool theory_seq::is_drop_last(expr* s, expr* i, expr* l) {
@@ -4857,6 +4860,7 @@ bool theory_seq::is_extract_suffix(expr* s, expr* i, expr* l) {
 /*
   0 <= l <= len(s) => s = ey & l = len(e)
   len(s) < l => s = e
+  l < 0 => e = empty
  */
 void theory_seq::add_extract_prefix_axiom(expr* e, expr* s, expr* l) {
     TRACE("seq", tout << mk_pp(e, m) << " " << mk_pp(s, m) << " " << mk_pp(l, m) << "\n";);
@@ -4872,12 +4876,13 @@ void theory_seq::add_extract_prefix_axiom(expr* e, expr* s, expr* l) {
     add_axiom(~l_ge_0, ~l_le_s, mk_eq(l, le, false));
     add_axiom(~l_ge_0, ~l_le_s, mk_eq(ls_minus_l, mk_len(y), false));
     add_axiom(l_le_s, mk_eq(e, s, false));
+    add_axiom(l_ge_0, mk_eq_empty(e));
 }
 
 /*
   0 <= i <= len(s) => s = xe & i = len(x)    
-  i < 0 => len(e) = 0
-  i > len(s) => len(e) = 0
+  i < 0 => e = empty
+  i > len(s) => e = empty
  */
 void theory_seq::add_extract_suffix_axiom(expr* e, expr* s, expr* i) {
     expr_ref x(mk_skolem(m_pre, s, i), m);
@@ -4885,7 +4890,7 @@ void theory_seq::add_extract_suffix_axiom(expr* e, expr* s, expr* i) {
     expr_ref ls = mk_len(s);
     expr_ref zero(m_autil.mk_int(0), m);
     expr_ref xe = mk_concat(x, e);
-    literal le_is_0 = mk_eq(zero, mk_len(e), false);
+    literal le_is_0 = mk_eq_empty(e);
     literal i_ge_0 = mk_simplified_literal(m_autil.mk_ge(i, zero));
     literal i_le_s = mk_simplified_literal(m_autil.mk_le(mk_sub(i, ls), zero));
     add_axiom(~i_ge_0, ~i_le_s, mk_seq_eq(s, xe));