diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 80d125c32..1cbc2d288 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -29,12 +29,27 @@ Notes:
 expr_ref sym_expr::accept(expr* e) {
     ast_manager& m = m_t.get_manager();
     expr_ref result(m);
-    if (m_is_pred) {
+    switch (m_ty) {
+    case t_pred: {
         var_subst subst(m);
         subst(m_t, 1, &e, result);
+        break;
     }
-    else {
+    case t_char:
         result = m.mk_eq(e, m_t);
+        break;
+    case t_range: {
+        bv_util bv(m);
+        rational r1, r2, r3;
+        unsigned sz;
+        if (bv.is_numeral(m_t, r1, sz) && bv.is_numeral(e, r2, sz) && bv.is_numeral(m_s, r3, sz)) {
+            result = m.mk_bool_val((r1 <= r2) && (r2 <= r3));            
+        }
+        else {
+            result = m.mk_and(bv.mk_ule(m_t, e), bv.mk_ule(e, m_s));
+        }
+        break;
+    }
     }
     return result;
 }
@@ -104,8 +119,7 @@ eautomaton* re2automaton::re2aut(expr* e) {
             expr_ref v(m.mk_var(0, s), m);
             expr_ref _start(bv.mk_numeral(start, nb), m);
             expr_ref _stop(bv.mk_numeral(stop, nb), m);
-            expr_ref cond(m.mk_and(bv.mk_ule(_start, v), bv.mk_ule(v, _stop)), m);
-            a = alloc(eautomaton, sm, sym_expr::mk_pred(cond));
+            a = alloc(eautomaton, sm, sym_expr::mk_range(_start, _stop));
             return a.detach();
         }
         else {
@@ -703,7 +717,8 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
 void seq_rewriter::add_next(u_map<expr*>& next, expr_ref_vector& trail, unsigned idx, expr* cond) {
     expr* acc;
     if (!m().is_true(cond) && next.find(idx, acc)) {              
-        cond = m().mk_or(cond, acc);
+        expr* args[2] = { cond, acc };
+        cond = mk_or(m(), 2, args);
     }
     trail.push_back(cond);
     next.insert(idx, cond);   
@@ -817,7 +832,7 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
             aut->get_moves_from(state, mvs, false);
             for (unsigned j = 0; j < mvs.size(); ++j) {
                 eautomaton::move const& mv = mvs[j];
-				SASSERT(mv.t());
+                SASSERT(mv.t());
                 if (mv.t()->is_char() && m().is_value(mv.t()->get_char()) && m().is_value(ch)) {
                     if (mv.t()->get_char() == ch) {
                         add_next(next, trail, mv.dst(), acc);
@@ -828,7 +843,11 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
                 }
                 else {
                     cond = mv.t()->accept(ch);
-                    if (!m().is_true(acc)) cond = m().mk_and(acc, cond);
+                    if (m().is_false(cond)) {
+                        continue;
+                    }
+                    expr* args[2] = { cond, acc };
+                    cond = mk_and(m(), 2, args);
                     add_next(next, trail, mv.dst(), cond);
                 }
             }                
@@ -856,18 +875,18 @@ br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) {
     return BR_FAILED;
 }
 br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) {
-	if (m_util.re.is_full(a) && m_util.re.is_full(b)) {
-		result = a;
-		return BR_DONE;
-	}
-	if (m_util.re.is_empty(a)) {
-		result = a;
-		return BR_DONE;
-	}
-	if (m_util.re.is_empty(b)) {
-		result = b;
-		return BR_DONE;
-	}
+    if (m_util.re.is_full(a) && m_util.re.is_full(b)) {
+        result = a;
+        return BR_DONE;
+    }
+    if (m_util.re.is_empty(a)) {
+        result = a;
+        return BR_DONE;
+    }
+    if (m_util.re.is_empty(b)) {
+        result = b;
+        return BR_DONE;
+    }
     if (is_epsilon(a)) {
         result = b;
         return BR_DONE;
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index f65b22b12..89cbb2566 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -27,20 +27,27 @@ Notes:
 #include"automaton.h"
 
 class sym_expr {
-    bool     m_is_pred;
+    enum ty {
+        t_char,
+        t_pred,
+        t_range
+    };
+    ty       m_ty;
     expr_ref m_t;
+    expr_ref m_s;
     unsigned m_ref;
-    sym_expr(bool is_pred, expr_ref& t) : m_is_pred(is_pred), m_t(t), m_ref(0) {}
+    sym_expr(ty ty, expr_ref& t, expr_ref& s) : m_ty(ty), m_t(t), m_s(s), m_ref(0) {}
 public:
     expr_ref accept(expr* e);
-    static sym_expr* mk_char(expr_ref& t) { return alloc(sym_expr, false, t); }
-    static sym_expr* mk_char(ast_manager& m, expr* t) { expr_ref tr(t, m); return alloc(sym_expr, false, tr); }
-    static sym_expr* mk_pred(expr_ref& t) { return alloc(sym_expr, true, t); }
+    static sym_expr* mk_char(expr_ref& t) { return alloc(sym_expr, t_char, t, t); }
+    static sym_expr* mk_char(ast_manager& m, expr* t) { expr_ref tr(t, m); return mk_char(tr); }
+    static sym_expr* mk_pred(expr_ref& t) { return alloc(sym_expr, t_pred, t, t); }
+    static sym_expr* mk_range(expr_ref& lo, expr_ref& hi) { return alloc(sym_expr, t_range, lo, hi); }
     void inc_ref() { ++m_ref;  }
     void dec_ref() { --m_ref; if (m_ref == 0) dealloc(this); }
     std::ostream& display(std::ostream& out) const;
-    bool is_char() const { return !m_is_pred; }
-    bool is_pred() const { return m_is_pred; }
+    bool is_char() const { return m_ty == t_char; }
+    bool is_pred() const { return !is_char(); }
     expr* get_char() const { SASSERT(is_char()); return m_t; }
 
 };
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 4ac7e8f7e..07ddf3886 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -634,15 +634,12 @@ void theory_seq::enforce_length_coherence(enode* n1, enode* n2) {
     expr* o1 = n1->get_owner();
     expr* o2 = n2->get_owner();
     if (m_util.str.is_concat(o1) && m_util.str.is_concat(o2)) {
-        //std::cout << "concats:\n" << mk_pp(o1,m) << "\n" << mk_pp(o2,m) << "\n";
         return;
     }
     if (has_length(o1) && !has_length(o2)) {
-        //std::cout << "enforce length: " << mk_pp(o1,m) << " -> " << mk_pp(o2,m) << "\n";
         enforce_length(n2);
     }
     else if (has_length(o2) && !has_length(o1)) {
-        //std::cout << "enforce length: " << mk_pp(o2,m) << " -> " << mk_pp(o1,m) << "\n";
         enforce_length(n1);
     }
 }
@@ -835,7 +832,6 @@ bool theory_seq::propagate_max_length(expr* l, expr* r, dependency* deps) {
     }
     rational hi;
     if (is_tail(l, s, idx) && has_length(s) && m_util.str.is_empty(r) && !upper_bound(s, hi)) {
-        //std::cout << "max length " << mk_pp(s, m) << " " << idx << "\n";
         propagate_lit(deps, 0, 0, mk_literal(m_autil.mk_le(m_util.str.mk_length(s), m_autil.mk_int(idx+1))));
         return true;
     }
@@ -1008,7 +1004,7 @@ bool theory_seq::solve_ne(unsigned idx) {
             }
             TRACE("seq", 
                   for (unsigned j = 0; j < lhs.size(); ++j) {
-                      tout << mk_pp(lhs[j].get(), m) << " ";
+                      tout << mk_pp(lhs[j].get(), m) << " " << mk_pp(rhs[j].get(), m) << "\n";
                   }
                   tout << "\n";
                   tout << n.ls(i) << " != " << n.rs(i) << "\n";);
@@ -1018,10 +1014,9 @@ bool theory_seq::solve_ne(unsigned idx) {
                 expr* nr = rhs[j].get();
                 if (m_util.is_seq(nl) || m_util.is_re(nl)) {
                     ls.reset();
-                     rs.reset(); 
-                    SASSERT(!m_util.str.is_concat(nl));
-                    SASSERT(!m_util.str.is_concat(nr));
-                    ls.push_back(nl); rs.push_back(nr);
+                    rs.reset(); 
+                    m_util.str.get_concat(nl, ls);
+                    m_util.str.get_concat(nr, rs);
                     new_ls.push_back(ls);
                     new_rs.push_back(rs);
                 }
@@ -1240,7 +1235,7 @@ void theory_seq::display_deps(std::ostream& out, dependency* dep) const {
     for (unsigned i = 0; i < lits.size(); ++i) {
         literal lit = lits[i];
         get_context().display_literals_verbose(out << "   ", 1, &lit);
-        tout << "\n";
+        out << "\n";
     }
 }