diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 1635ea7bb..b353499ad 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -205,6 +205,18 @@ namespace z3 {
            \brief Return the Bit-vector sort of size \c sz. That is, the sort for bit-vectors of size \c sz.
         */
         sort bv_sort(unsigned sz);
+        /**
+           \brief Return the sort for ASCII strings.
+         */
+        sort string_sort();
+        /**
+           \brief Return a sequence sort over base sort \c s.
+         */
+        sort seq_sort(sort& s);
+        /**
+           \brief Return a regular expression sort over sequences \c seq_sort.
+         */
+        sort re_sort(sort& seq_sort);
         /**
            \brief Return an array sort for arrays from \c d to \c r.
 
@@ -261,6 +273,9 @@ namespace z3 {
         expr bv_val(__uint64 n, unsigned sz);
         expr bv_val(char const * n, unsigned sz);
 
+        expr string_val(char const* s);
+        expr string_val(std::string const& s);
+
         expr num_val(int n, sort const & s);
 
         /**
@@ -425,6 +440,14 @@ namespace z3 {
             \brief Return true if this sort is a Relation sort.
         */
         bool is_relation() const { return sort_kind() == Z3_RELATION_SORT; }
+        /**
+            \brief Return true if this sort is a Sequence sort.
+        */
+        bool is_seq() const { return sort_kind() == Z3_SEQ_SORT; }
+        /**
+            \brief Return true if this sort is a regular expression sort.
+        */
+        bool is_re() const { return sort_kind() == Z3_RE_SORT; }
         /**
             \brief Return true if this sort is a Finite domain sort.
         */
@@ -532,6 +555,15 @@ namespace z3 {
            \brief Return true if this is a Relation expression.
         */
         bool is_relation() const { return get_sort().is_relation(); }
+        /**
+           \brief Return true if this is a sequence expression.
+        */
+        bool is_seq() const { return get_sort().is_seq(); }
+        /**
+           \brief Return true if this is a regular expression.
+        */
+        bool is_re() const { return get_sort().is_re(); }
+        
         /**
            \brief Return true if this is a Finite-domain expression.
 
@@ -663,6 +695,7 @@ namespace z3 {
 
         friend expr distinct(expr_vector const& args);
         friend expr concat(expr const& a, expr const& b);
+        friend expr concat(expr_vector const& args);
 
         friend expr operator==(expr const & a, expr const & b);
         friend expr operator==(expr const & a, int b);
@@ -728,10 +761,50 @@ namespace z3 {
         friend expr operator|(int a, expr const & b);
 
         friend expr operator~(expr const & a);
-        expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); return expr(ctx(), r); }
+        expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }        
         unsigned lo() const { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 1)); }
         unsigned hi() const { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 0)); }
 
+        /**
+           \brief sequence and regular expression operations.
+           + is overloaeded as sequence concatenation and regular expression union.
+           concat is overloaded to handle sequences and regular expressions
+        */
+        expr extract(expr const& offset, expr const& length) const { 
+            check_context(*this, offset); check_context(offset, length);
+            Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r); 
+        }
+        expr replace(expr const& src, expr const& dst) const {
+            check_context(*this, src); check_context(src, dst);
+            Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
+            check_error();
+            return expr(ctx(), r);
+        }
+        expr unit() const {
+            Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
+            check_error();
+            return expr(ctx(), r);
+        }
+        expr contains(expr const& s) {
+            check_context(*this, s);
+            Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
+            check_error();
+            return expr(ctx(), r);
+        }
+        expr at(expr const& index) const {
+            check_context(*this, index);
+            Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
+            check_error();
+            return expr(ctx(), r);
+        }
+        expr length() const {
+            Z3_ast r = Z3_mk_seq_length(ctx(), *this);
+            check_error();
+            return expr(ctx(), r);
+        }
+
+
+
         /**
            \brief Return a simplified version of this expression.
         */
@@ -835,6 +908,13 @@ namespace z3 {
         else if (a.is_bv() && b.is_bv()) {
             r = Z3_mk_bvadd(a.ctx(), a, b);
         }
+        else if (a.is_seq() && b.is_seq()) {
+            return concat(a, b);
+        }
+        else if (a.is_re() && b.is_re()) {
+            Z3_ast _args[2] = { a, b };
+            r = Z3_mk_re_union(a.ctx(), 2, _args);
+        }
         else {
             // operator is not supported by given arguments.
             assert(false);
@@ -1219,11 +1299,48 @@ namespace z3 {
 
     inline expr concat(expr const& a, expr const& b) {
         check_context(a, b);
-        Z3_ast r = Z3_mk_concat(a.ctx(), a, b);
+        Z3_ast r;
+        if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
+            Z3_ast _args[2] = { a, b };
+            r = Z3_mk_seq_concat(a.ctx(), 2, _args);
+        }
+        else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
+            Z3_ast _args[2] = { a, b };
+            r = Z3_mk_re_concat(a.ctx(), 2, _args);
+        }
+        else {
+            r = Z3_mk_concat(a.ctx(), a, b);
+        }
         a.ctx().check_error();
         return expr(a.ctx(), r);
     }
 
+    inline expr concat(expr_vector const& args) {
+        Z3_ast r;
+        assert(args.size() > 0);
+        if (args.size() == 1) {
+            return args[0];
+        }
+        context& ctx = args[0].ctx();
+        array<Z3_ast> _args(args);
+        if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
+            r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
+        }
+        else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
+            r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
+        }
+        else {
+            r = _args[args.size()-1];
+            for (unsigned i = args.size()-1; i > 0; ) {
+                --i;
+                r = Z3_mk_concat(ctx, _args[i], r);
+                ctx.check_error();
+            }
+        }
+        ctx.check_error();
+        return expr(ctx, r);
+    }
+
     class func_entry : public object {
         Z3_func_entry m_entry;
         void init(Z3_func_entry e) {
@@ -1762,6 +1879,10 @@ namespace z3 {
     inline sort context::int_sort() { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }
     inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
     inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
+    inline sort context::string_sort() { Z3_sort s = Z3_mk_string_sort(m_ctx); check_error(); return sort(*this, s); }
+    inline sort context::seq_sort(sort& s) { Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); }
+    inline sort context::re_sort(sort& s) { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
+
     inline sort context::array_sort(sort d, sort r) { Z3_sort s = Z3_mk_array_sort(m_ctx, d, r); check_error(); return sort(*this, s); }
     inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
         array<Z3_symbol> _enum_names(n);
@@ -1885,6 +2006,9 @@ namespace z3 {
     inline expr context::bv_val(__uint64 n, unsigned sz) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
     inline expr context::bv_val(char const * n, unsigned sz) { Z3_ast r = Z3_mk_numeral(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
 
+    inline expr context::string_val(char const* s) { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
+    inline expr context::string_val(std::string const& s) { Z3_ast r = Z3_mk_string(m_ctx, s.c_str()); check_error(); return expr(*this, r); }
+
     inline expr context::num_val(int n, sort const & s) { Z3_ast r = Z3_mk_int(m_ctx, n, s); check_error(); return expr(*this, r); }
 
     inline expr func_decl::operator()(unsigned n, expr const * args) const {
@@ -2017,6 +2141,62 @@ namespace z3 {
         d.check_error();
         return expr(d.ctx(), r);
     }
+
+    // sequence and regular expression operations.
+    // union is +
+    // concat is overloaded to handle sequences and regular expressions
+
+    inline expr empty(sort const& s) {
+        Z3_ast r = Z3_mk_seq_empty(s.ctx(), s);
+        s.check_error();
+        return expr(s.ctx(), r);
+    }
+    inline expr suffixof(expr const& a, expr const& b) {
+        check_context(a, b);
+        Z3_ast r = Z3_mk_seq_suffix(a.ctx(), a, b);
+        a.check_error();
+        return expr(a.ctx(), r);
+    }
+    inline expr prefixof(expr const& a, expr const& b) {
+        check_context(a, b);
+        Z3_ast r = Z3_mk_seq_prefix(a.ctx(), a, b);
+        a.check_error();
+        return expr(a.ctx(), r);
+    }
+    inline expr indexof(expr const& s, expr const& substr, expr const& offset) {
+        check_context(s, substr); check_context(s, offset);
+        Z3_ast r = Z3_mk_seq_index(s.ctx(), s, substr, offset);
+        s.check_error();
+        return expr(s.ctx(), r);
+    }
+    inline expr to_re(expr const& s) {
+        Z3_ast r = Z3_mk_seq_to_re(s.ctx(), s);
+        s.check_error();
+        return expr(s.ctx(), r);
+    }
+    inline expr in_re(expr const& s, expr const& re) {
+        check_context(s, re);
+        Z3_ast r = Z3_mk_seq_in_re(s.ctx(), s, re);
+        s.check_error();
+        return expr(s.ctx(), r);
+    }
+    inline expr plus(expr const& re) {
+        Z3_ast r = Z3_mk_re_plus(re.ctx(), re);
+        re.check_error();
+        return expr(re.ctx(), r);
+    }
+    inline expr option(expr const& re) {
+        Z3_ast r = Z3_mk_re_option(re.ctx(), re);
+        re.check_error();
+        return expr(re.ctx(), r);
+    }
+    inline expr star(expr const& re) {
+        Z3_ast r = Z3_mk_re_star(re.ctx(), re);
+        re.check_error();
+        return expr(re.ctx(), r);
+    }
+
+
     inline expr interpolant(expr const& a) {
         return expr(a.ctx(), Z3_mk_interpolant(a.ctx(), a));
     }
diff --git a/src/math/automata/automaton.h b/src/math/automata/automaton.h
index f64dfd205..2a4c964f9 100644
--- a/src/math/automata/automaton.h
+++ b/src/math/automata/automaton.h
@@ -292,7 +292,8 @@ public:
     // Generalized: 
     // Src - E -> dst - t -> dst1 => Src - t -> dst1   if dst is final => each Src is final
     //
-    // src - e -> dst - ET -> dst1 => src - ET - dst1  if in_degree(dst) = 1, src != dst
+    // src - e -> dst - ET -> Dst1 => src - ET -> Dst1  if in_degree(dst) = 1, src != dst
+    // Src - E -> dst - et -> dst1 => Src - et -> dst1  if out_degree(dst) = 1, src != dst
     // 
     void compress() {
         for (unsigned i = 0; i < m_delta.size(); ++i) {
@@ -339,24 +340,42 @@ public:
                             add(mvs1[k]);
                         }
                     }
-                    else if (false && 1 == out_degree(dst) && all_epsilon_in(dst) && init() != dst && !is_final_state(dst)) {
+                    //
+                    // Src - E -> dst - et -> dst1 => Src - et -> dst1  if out_degree(dst) = 1, src != dst
+                    //
+                    else if (1 == out_degree(dst) && all_epsilon_in(dst) && init() != dst && !is_final_state(dst)) {
                         move const& mv = m_delta[dst][0];
-                        T* t = mv.t();
                         unsigned dst1 = mv.dst();
+                        T* t = mv.t();
                         unsigned_vector src0s;
                         moves const& mvs = m_delta_inv[dst];
+                        moves mvs1;
                         for (unsigned k = 0; k < mvs.size(); ++k) {
                             SASSERT(mvs[k].is_epsilon());
-                            src0s.push_back(mvs[k].src());
+                            mvs1.push_back(move(m, mvs[k].src(), dst1, t));
                         }
-                        for (unsigned k = 0; k < src0s.size(); ++k) {
-                            remove(src0s[k], dst, 0);
-                            add(move(m, src0s[i], dst1, t));
+                        for (unsigned k = 0; k < mvs1.size(); ++k) {
+                            remove(mvs1[k].src(), dst, 0);
+                            add(mvs1[k]);
                         }
                         remove(dst, dst1, t);    
                         --j;
                         continue;
                     }
+                    //
+                    // Src1 - ET -> src - e -> dst => Src1 - ET -> dst  if out_degree(src) = 1, src != init() 
+                    //
+                    else if (1 == out_degree(src) && init() != src && (!is_final_state(src) || is_final_state(dst))) {
+                        moves const& mvs = m_delta_inv[src];
+                        moves mvs1;
+                        for (unsigned k = 0; k < mvs.size(); ++k) {
+                            mvs1.push_back(move(m, mvs[k].src(), dst, mvs[k].t()));
+                        }
+                        for (unsigned k = 0; k < mvs1.size(); ++k) {
+                            remove(mvs1[k].src(), src, mvs1[k].t());
+                            add(mvs1[k]);
+                        }
+                    }
                     else {
                         continue;
                     }                    
@@ -482,7 +501,7 @@ private:
     void remove_dead_states() {
         unsigned_vector remap;
         for (unsigned i = 0; i < m_delta.size(); ++i) {
-
+            
         }
     }    
 
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 1f3afa672..88988d2b4 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -373,14 +373,12 @@ bool theory_seq::propagate_length_coherence(expr* e) {
         expr_ref high1(m_autil.mk_le(m_util.str.mk_length(e), m_autil.mk_numeral(hi, true)), m);
         expr_ref high2(m_autil.mk_le(m_util.str.mk_length(seq), m_autil.mk_numeral(hi-lo, true)), m);     
         add_axiom(~mk_literal(high1), mk_literal(high2));
-        m_trail_stack.push(push_replay(alloc(replay_length_coherence, m, e)));
     }
-
+    m_trail_stack.push(push_replay(alloc(replay_length_coherence, m, e)));
     return true;
 }
 
 bool theory_seq::check_length_coherence() {
-    bool coherent = true;
     obj_hashtable<expr>::iterator it = m_length.begin(), end = m_length.end();
     for (; it != end; ++it) {
         expr* e = *it;
@@ -398,7 +396,7 @@ bool theory_seq::check_length_coherence() {
             return false;
         }
     }
-    return coherent;
+    return true;
 }    
 
 /*
@@ -890,6 +888,23 @@ void theory_seq::solve_ne(unsigned idx) {
         set_conflict(n.m_dep, lits);
         SASSERT(m_new_propagation);
     }
+    if (num_undef_lits == 0 && n.m_lhs.size() == 1) {
+        expr* l = n.m_lhs[0];
+        expr* r = n.m_rhs[0];
+        if (m_util.str.is_empty(r)) {
+            std::swap(l, r);
+        }
+        if (m_util.str.is_empty(l) && is_var(r)) {
+            literal lit = ~mk_eq_empty(r);
+            if (ctx.get_assignment(lit) == l_true) {
+                expr_ref head(m), tail(m);
+                mk_decompose(r, head, tail);
+                expr_ref conc(m_util.str.mk_concat(head, tail), m);
+                propagate_is_conc(r, conc);
+            }
+            m_new_propagation = true;            
+        }
+    }
 }
 
 
@@ -2171,6 +2186,15 @@ bool theory_seq::add_accept2step(expr* acc) {
             break;
         }
     }
+    if (has_undef && mvs.size() == 1) {
+        literal lit = lits.back();
+        lits.pop_back();
+        for (unsigned i = 0; i < lits.size(); ++i) {
+            lits[i].neg();
+        }
+        propagate_lit(0, lits.size(), lits.c_ptr(), lit);
+        return false;
+    }
     if (has_undef) {
         return true;
     }