diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index ed5df106b..3ca0012e7 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -460,7 +460,7 @@ def find_ocaml_find():
         print ("Testing %s..." % OCAMLFIND)
     r = exec_cmd([OCAMLFIND, 'printconf'])
     if r != 0:
-        OCAMLFIND=''
+        OCAMLFIND = ''
 
 def find_ml_lib():
     global OCAML_LIB
@@ -630,6 +630,7 @@ def display_help(exit_code):
     print("  JDK_HOME   JDK installation directory (only relevant if -j or --java option is provided)")
     print("  JNI_HOME   JNI bindings directory (only relevant if -j or --java option is provided)")
     print("  OCAMLC     Ocaml byte-code compiler (only relevant with --ml)")
+    print("  OCAMLFIND  Ocaml find tool (only relevant with --ml)")
     print("  OCAMLOPT   Ocaml native compiler (only relevant with --ml)")
     print("  OCAML_LIB  Ocaml library directory (only relevant with --ml)")
     print("  CSC        C# Compiler (only relevant if .NET bindings are enabled)")
@@ -1753,6 +1754,42 @@ class MLComponent(Component):
         self.stubs = "z3native_stubs"
         self.sub_dir = os.path.join('api', 'ml')
 
+        self.destdir = ""
+        self.ldconf = ""
+        # Calling _init_ocamlfind_paths() is postponed to later because
+        # OCAMLFIND hasn't been checked yet.
+
+    def _install_bindings(self):
+        # FIXME: Depending on global state is gross.  We can't pre-compute this
+        # in the constructor because we haven't tested for ocamlfind yet
+        return OCAMLFIND != ''
+
+    def _init_ocamlfind_paths(self):
+        """
+            Initialises self.destdir and self.ldconf
+
+            Do not call this from the MLComponent constructor because OCAMLFIND
+            has not been checked at that point
+        """
+        if self.destdir != "" and self.ldconf != "":
+            # Initialisation already done
+            return
+        # Use Ocamlfind to get the default destdir and ldconf path
+        self.destdir = check_output([OCAMLFIND, 'printconf', 'destdir'])
+        if self.destdir == "":
+            raise MKException('Failed to get OCaml destdir')
+
+        if not os.path.isdir(self.destdir):
+            raise MKException('The destdir reported by {ocamlfind} ({destdir}) does not exist'.format(ocamlfind=OCAMLFIND, destdir=self.destdir))
+
+        self.ldconf = check_output([OCAMLFIND, 'printconf', 'ldconf'])
+        if self.ldconf == "":
+            raise MKException('Failed to get OCaml ldconf path')
+
+    def final_info(self):
+        if not self._install_bindings():
+            print("WARNING: Could not find ocamlfind utility. OCaml bindings will not be installed")
+
     def mk_makefile(self, out):
         if is_ml_enabled():
             src_dir = self.to_src_dir
@@ -1832,7 +1869,7 @@ class MLComponent(Component):
                 out.write('\n')
 
     def mk_install_deps(self, out):
-        if is_ml_enabled() and OCAMLFIND != '':
+        if is_ml_enabled() and self._install_bindings():
             out.write(get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT) ')
             out.write(os.path.join(self.sub_dir, 'META '))
             out.write(os.path.join(self.sub_dir, 'z3ml.cma '))
@@ -1840,8 +1877,22 @@ class MLComponent(Component):
             out.write(os.path.join(self.sub_dir, 'z3ml.cmxs '))
 
     def mk_install(self, out):
-        if is_ml_enabled() and OCAMLFIND != '':
-            out.write('\t@%s install Z3 %s' % (OCAMLFIND, (os.path.join(self.sub_dir, 'META'))))
+        if is_ml_enabled() and self._install_bindings():
+            self._init_ocamlfind_paths()
+            in_prefix = self.destdir.startswith(PREFIX)
+            maybe_stripped_destdir = strip_path_prefix(self.destdir, PREFIX)
+            # Note that when doing a staged install with DESTDIR that modifying
+            # OCaml's ``ld.conf`` may fail. Therefore packagers will need to
+            # make their packages modify it manually at package install time
+            # as opposed to ``make install`` time.
+            MakeRuleCmd.make_install_directory(out,
+                                               maybe_stripped_destdir,
+                                               in_prefix=in_prefix)
+            out.write('\t@{ocamlfind} install -ldconf $(DESTDIR){ldconf} -destdir $(DESTDIR){ocaml_destdir} Z3 {metafile}'.format(
+                ldconf=self.ldconf,
+                ocamlfind=OCAMLFIND,
+                ocaml_destdir=self.destdir,
+                metafile=os.path.join(self.sub_dir, 'META')))
 
             for m in self.modules:
                 out.write(' ' + os.path.join(self.to_src_dir, m) + '.mli')
@@ -1859,8 +1910,12 @@ class MLComponent(Component):
             out.write('\n')
 
     def mk_uninstall(self, out):
-        if is_ml_enabled() and OCAMLFIND != '':
-            out.write('\t@%s remove Z3\n' % (OCAMLFIND))
+        if is_ml_enabled() and self._install_bindings():
+            self._init_ocamlfind_paths()
+            out.write('\t@{ocamlfind} remove -ldconf $(DESTDIR){ldconf} -destdir $(DESTDIR){ocaml_destdir} Z3\n'.format(
+                ldconf=self.ldconf,
+                ocamlfind=OCAMLFIND,
+                ocaml_destdir=self.destdir))
 
     def main_component(self):
         return is_ml_enabled()
@@ -2175,6 +2230,7 @@ def mk_config():
                 print('Java Compiler:  %s' % JAVAC)
             if is_ml_enabled():
                 print('OCaml Compiler: %s' % OCAMLC)
+                print('OCaml Find tool: %s' % OCAMLFIND)
                 print('OCaml Native:   %s' % OCAMLOPT)
                 print('OCaml Library:  %s' % OCAML_LIB)
     else:
@@ -2310,6 +2366,7 @@ def mk_config():
                 print('Java Compiler:  %s' % JAVAC)
             if is_ml_enabled():
                 print('OCaml Compiler: %s' % OCAMLC)
+                print('OCaml Find tool: %s' % OCAMLFIND)
                 print('OCaml Native:   %s' % OCAMLOPT)
                 print('OCaml Library:  %s' % OCAML_LIB)
             if is_dotnet_enabled():
@@ -3535,6 +3592,15 @@ class MakeRuleCmd(object):
         # Note: DESTDIR is to support staged installs
         return "$(DESTDIR)$(PREFIX)/"
 
+    @classmethod
+    def _is_str(cls, obj):
+        if sys.version_info.major > 2:
+            # Python 3 or newer. Strings are always unicode and of type str
+            return isinstance(obj, str)
+        else:
+            # Python 2. Has byte-string and unicode representation, allow both
+            return isinstance(obj, str) or isinstance(obj, unicode)
+
     @classmethod
     def _install_root(cls, path, in_prefix, out, is_install=True):
         if not in_prefix:
@@ -3553,9 +3619,9 @@ class MakeRuleCmd(object):
     @classmethod
     def install_files(cls, out, src_pattern, dest, in_prefix=True):
         assert len(dest) > 0
-        assert isinstance(src_pattern, str)
+        assert cls._is_str(src_pattern)
         assert not ' ' in src_pattern
-        assert isinstance(dest, str)
+        assert cls._is_str(dest)
         assert not ' ' in dest
         assert not os.path.isabs(src_pattern)
         install_root = cls._install_root(dest, in_prefix, out)
@@ -3568,7 +3634,7 @@ class MakeRuleCmd(object):
     @classmethod
     def remove_installed_files(cls, out, pattern, in_prefix=True):
         assert len(pattern) > 0
-        assert isinstance(pattern, str)
+        assert cls._is_str(pattern)
         assert not ' ' in pattern
         install_root = cls._install_root(pattern, in_prefix, out, is_install=False)
 
@@ -3579,7 +3645,7 @@ class MakeRuleCmd(object):
     @classmethod
     def make_install_directory(cls, out, dir, in_prefix=True):
         assert len(dir) > 0
-        assert isinstance(dir, str)
+        assert cls._is_str(dir)
         assert not ' ' in dir
         install_root = cls._install_root(dir, in_prefix, out)
 
@@ -3593,8 +3659,8 @@ class MakeRuleCmd(object):
             Returns True iff ``temp_path`` is a path prefix
             of ``target_as_abs``
         """
-        assert isinstance(temp_path, str)
-        assert isinstance(target_as_abs, str)
+        assert cls._is_str(temp_path)
+        assert cls._is_str(target_as_abs)
         assert len(temp_path) > 0
         assert len(target_as_abs) > 0
         assert os.path.isabs(temp_path)
@@ -3610,8 +3676,8 @@ class MakeRuleCmd(object):
 
     @classmethod
     def create_relative_symbolic_link(cls, out, target, link_name):
-        assert isinstance(target, str)
-        assert isinstance(link_name, str)
+        assert cls._is_str(target)
+        assert cls._is_str(link_name)
         assert len(target) > 0
         assert len(link_name) > 0
         assert not os.path.isabs(target)
@@ -3648,8 +3714,8 @@ class MakeRuleCmd(object):
 
     @classmethod
     def create_symbolic_link(cls, out, target, link_name):
-        assert isinstance(target, str)
-        assert isinstance(link_name, str)
+        assert cls._is_str(target)
+        assert cls._is_str(link_name)
         assert not os.path.isabs(target)
 
         cls.write_cmd(out, 'ln -s {target} {install_root}{link_name}'.format(
diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp
index 90b818b4b..eaffdd226 100644
--- a/src/api/api_fpa.cpp
+++ b/src/api/api_fpa.cpp
@@ -943,7 +943,7 @@ extern "C" {
             return "";
         }
         scoped_mpf val(mpfm);
-        app * a = to_app(e);
+//        app * a = to_app(e);
         bool r = plugin->is_numeral(e, val);
         if (!r || !mpfm.is_regular(val)) {
             SET_ERROR_CODE(Z3_INVALID_ARG)
@@ -981,7 +981,7 @@ extern "C" {
             return 0;
         }
         scoped_mpf val(mpfm);
-        app * a = to_app(e);
+//        app * a = to_app(e);
         bool r = plugin->is_numeral(e, val);
         const mpz & z = mpfm.sig(val);
         if (!r || mpfm.is_regular(val)|| !mpzm.is_uint64(z)) {
@@ -1012,7 +1012,7 @@ extern "C" {
             return "";
         }
         scoped_mpf val(mpfm);
-        app * a = to_app(e);
+//        app * a = to_app(e);
         bool r = plugin->is_numeral(e, val);
         if (!r || !mpfm.is_regular(val)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
@@ -1044,7 +1044,7 @@ extern "C" {
             return 0;
         }
         scoped_mpf val(mpfm);
-        app * a = to_app(e);
+//        app * a = to_app(e);
         bool r = plugin->is_numeral(e, val);
         if (!r || !mpfm.is_regular(val)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 2670dfa9a..0626d2f3c 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -9320,8 +9320,10 @@ def Union(*args):
     args = _get_args(args)
     sz = len(args)
     if __debug__:
-        _z3_assert(sz >= 2, "At least two arguments expected.")
+        _z3_assert(sz > 0, "At least one argument expected.")
         _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
+    if sz == 1:
+        return args[0]
     ctx = args[0].ctx
     v = (Ast * sz)()
     for i in range(sz):
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
index 102082cd5..16aef6a00 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
@@ -1171,7 +1171,6 @@ void bit_blaster_tpl<Cfg>::mk_carry_save_adder(unsigned sz, expr * const * a_bit
 
 template<typename Cfg>
 bool bit_blaster_tpl<Cfg>::mk_const_case_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
-    unsigned nb = 0;
     unsigned case_size = 1;
     unsigned circuit_size = sz*sz*5;
     for (unsigned i = 0; case_size < circuit_size && i < sz; ++i) {
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index d94e54935..439d60bbf 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -24,26 +24,42 @@ Notes:
 #include"uint_set.h"
 #include"automaton.h"
 #include"well_sorted.h"
+#include"var_subst.h"
 
+expr_ref sym_expr::accept(expr* e) {
+    ast_manager& m = m_t.get_manager();
+    expr_ref result(m);
+    if (m_is_pred) {
+        var_subst subst(m);
+        subst(m_t, 1, &e, result);
+    }
+    else {
+        result = m.mk_eq(e, m_t);
+    }
+    return result;
+}
+
+std::ostream& sym_expr::display(std::ostream& out) const {
+    return out << m_t;
+}
 
 struct display_expr1 {
     ast_manager& m;
     display_expr1(ast_manager& m): m(m) {}
-    std::ostream& display(std::ostream& out, expr* e) const {
-        return out << mk_pp(e, m);
+    std::ostream& display(std::ostream& out, sym_expr* e) const {
+        return e->display(out);
     }
 };
 
 
-re2automaton::re2automaton(ast_manager& m): m(m), u(m) {}
+re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m) {}
 
 eautomaton* re2automaton::operator()(expr* e) { 
     eautomaton* r = re2aut(e); 
     if (r) {
-        //display_expr1 disp(m);
-        //r->display(std::cout, disp);
+        display_expr1 disp(m);
         r->compress(); 
-        //r->display(std::cout, disp);
+        TRACE("seq", r->display(tout, disp););
     }
     return r;
 } 
@@ -53,6 +69,8 @@ eautomaton* re2automaton::re2aut(expr* e) {
     SASSERT(u.is_re(e));
     expr* e1, *e2;
     scoped_ptr<eautomaton> a, b;
+    unsigned lo, hi;
+    zstring s1, s2;
     if (u.re.is_to_re(e, e1)) {
         return seq2aut(e1);
     }
@@ -76,17 +94,45 @@ eautomaton* re2automaton::re2aut(expr* e) {
         a = eautomaton::mk_opt(*a);
         return a.detach();                    
     }
-    else if (u.re.is_range(e)) {
-
+    else if (u.re.is_range(e, e1, e2)) {
+        if (u.str.is_string(e1, s1) && u.str.is_string(e2, s2) &&
+            s1.length() == 1 && s2.length() == 1) {
+            unsigned start = s1[0];
+            unsigned stop = s2[0];
+            unsigned nb = s1.num_bits();
+            sort_ref s(bv.mk_sort(nb), m);          
+            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));
+            return a.detach();
+        }
+        else {
+            TRACE("seq", tout << "Range expression is not handled: " << mk_pp(e, m) << "\n";);
+        }
     }
-    else if (u.re.is_loop(e)) {
-
+    else if (u.re.is_loop(e, e1, lo, hi) && (a = re2aut(e1))) {
+        scoped_ptr<eautomaton> eps = eautomaton::mk_epsilon(sm);
+        b = eautomaton::mk_epsilon(sm);
+        while (hi > lo) {
+            scoped_ptr<eautomaton> c = eautomaton::mk_concat(*a, *b);
+            b = eautomaton::mk_union(*eps, *c);
+            --hi;
+        }
+        while (lo > 0) {
+            b = eautomaton::mk_concat(*a, *b);
+            --lo;
+        }
+        return b.detach();        
     }
 #if 0
-    else if (u.re.is_intersect(e, e1, e2)) {
-
-    }
     else if (u.re.is_empty(e)) {
+        return alloc(eautomaton, m);
+    }
+    else if (u.re.is_full(e)) {
+    }
+    else if (u.re.is_intersect(e, e1, e2)) {
 
     }
 #endif
@@ -103,10 +149,10 @@ eautomaton* re2automaton::seq2aut(expr* e) {
         return eautomaton::mk_concat(*a, *b);
     }
     else if (u.str.is_unit(e, e1)) {
-        return alloc(eautomaton, m, e1);
+        return alloc(eautomaton, sm, sym_expr::mk_char(m, e1));
     }
     else if (u.str.is_empty(e)) {
-        return eautomaton::mk_epsilon(m);
+        return eautomaton::mk_epsilon(sm);
     }
     else if (u.str.is_string(e, s)) {        
         unsigned init = 0;
@@ -115,9 +161,9 @@ eautomaton* re2automaton::seq2aut(expr* e) {
         final.push_back(s.length());
         for (unsigned k = 0; k < s.length(); ++k) {
             // reference count?
-            mvs.push_back(eautomaton::move(m, k, k+1, u.str.mk_char(s, k)));
+            mvs.push_back(eautomaton::move(sm, k, k+1, sym_expr::mk_char(m, u.str.mk_char(s, k))));
         }
-        return alloc(eautomaton, m, init, final, mvs);
+        return alloc(eautomaton, sm, init, final, mvs);
     }
     return 0;
 }
@@ -210,8 +256,6 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_STRING_STOI: 
         SASSERT(num_args == 1);
         return mk_str_stoi(args[0], result);
-    case OP_REGEXP_LOOP: 
-        return BR_FAILED;
     case _OP_STRING_CONCAT:
     case _OP_STRING_PREFIX:
     case _OP_STRING_SUFFIX:
@@ -653,7 +697,37 @@ void seq_rewriter::add_next(u_map<expr*>& next, unsigned idx, expr* cond) {
     }
 }
 
+bool seq_rewriter::is_sequence(eautomaton& aut, expr_ref_vector& seq) {
+    seq.reset();
+    unsigned state = aut.init();
+    uint_set visited;
+    eautomaton::moves mvs;
+    aut.get_moves_from(state, mvs, true);
+    while (!aut.is_final_state(state)) {
+        if (mvs.size() != 1) {
+            return false;
+        }
+        if (visited.contains(state)) {
+            return false;
+        }
+        if (aut.is_final_state(mvs[0].src())) {
+            return false;
+        }
+        visited.insert(state);
+        sym_expr* t = mvs[0].t();
+        if (!t || !t->is_char()) {
+            return false;
+        }
+        seq.push_back(m_util.str.mk_unit(t->get_char()));
+        state = mvs[0].dst();
+        mvs.reset();
+        aut.get_moves_from(state, mvs, true);
+    }
+    return mvs.empty();
+}
+
 bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
+    seq.reset();
     zstring s;
     ptr_vector<expr> todo;
     expr *e1, *e2;
@@ -688,63 +762,80 @@ bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
 br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
     scoped_ptr<eautomaton> aut;
     expr_ref_vector seq(m());
-    if (is_sequence(a, seq) && (aut = re2automaton(m())(b))) {
-        expr_ref_vector trail(m());
-        u_map<expr*> maps[2];
-        bool select_map = false;
-        expr_ref ch(m()), cond(m());
-        eautomaton::moves mvs;
-        maps[0].insert(aut->init(), m().mk_true());
-        // is_accepted(a, aut) & some state in frontier is final.
+    if (!(aut = m_re2aut(b))) {
+        return BR_FAILED;
+    }
 
-        for (unsigned i = 0; i < seq.size(); ++i) {
-            u_map<expr*>& frontier = maps[select_map];
-            u_map<expr*>& next = maps[!select_map];
-            select_map = !select_map;
-            ch = seq[i].get();
-            next.reset();
-            u_map<expr*>::iterator it = frontier.begin(), end = frontier.end();
-            for (; it != end; ++it) {
-                mvs.reset();
-                unsigned state = it->m_key;
-                expr*    acc  = it->m_value;
-                aut->get_moves_from(state, mvs, false);
-                for (unsigned j = 0; j < mvs.size(); ++j) {
-                    eautomaton::move const& mv = mvs[j];
-                    if (m().is_value(mv.t()) && m().is_value(ch)) {
-                        if (mv.t() == ch) {
-                            add_next(next, mv.dst(), acc);
-                        }
-                        else {
-                            continue;
-                        }
-                    }
-                    else {
-                        cond = m().mk_eq(mv.t(), ch);
-                        if (!m().is_true(acc)) cond = m().mk_and(acc, cond);
-                        add_next(next, mv.dst(), cond);
-                    }
-                }                
-            }
+    if (is_sequence(*aut, seq)) {
+        TRACE("seq", tout << seq << "\n";);
+              
+        if (seq.empty()) {
+            result = m().mk_eq(a, m_util.str.mk_empty(m().get_sort(a)));
         }
-        u_map<expr*> const& frontier = maps[select_map];
-        u_map<expr*>::iterator it = frontier.begin(), end = frontier.end();
-        expr_ref_vector ors(m());
-        for (; it != end; ++it) {
-            unsigned_vector states;
-            bool has_final = false;
-            aut->get_epsilon_closure(it->m_key, states);
-            for (unsigned i = 0; i < states.size() && !has_final; ++i) {
-                has_final = aut->is_final_state(states[i]);
-            }
-            if (has_final) {
-                ors.push_back(it->m_value);
-            }
+        else {
+            result = m().mk_eq(a, m_util.str.mk_concat(seq));
         }
-        result = mk_or(ors);
         return BR_REWRITE_FULL;
     }
-    return BR_FAILED;
+
+    if (!is_sequence(a, seq)) {
+        return BR_FAILED;
+    } 
+        
+    expr_ref_vector trail(m());
+    u_map<expr*> maps[2];
+    bool select_map = false;
+    expr_ref ch(m()), cond(m());
+    eautomaton::moves mvs;
+    maps[0].insert(aut->init(), m().mk_true());
+    // is_accepted(a, aut) & some state in frontier is final.
+    
+    for (unsigned i = 0; i < seq.size(); ++i) {
+        u_map<expr*>& frontier = maps[select_map];
+        u_map<expr*>& next = maps[!select_map];
+        select_map = !select_map;
+        ch = seq[i].get();
+        next.reset();
+        u_map<expr*>::iterator it = frontier.begin(), end = frontier.end();
+        for (; it != end; ++it) {
+            mvs.reset();
+            unsigned state = it->m_key;
+            expr*    acc  = it->m_value;
+            aut->get_moves_from(state, mvs, false);
+            for (unsigned j = 0; j < mvs.size(); ++j) {
+                eautomaton::move const& mv = mvs[j];
+                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, mv.dst(), acc);
+                    }
+                    else {
+                        continue;
+                    }
+                }
+                else {
+                    cond = mv.t()->accept(ch);
+                    if (!m().is_true(acc)) cond = m().mk_and(acc, cond);
+                    add_next(next, mv.dst(), cond);
+                }
+            }                
+        }
+    }
+    u_map<expr*> const& frontier = maps[select_map];
+    u_map<expr*>::iterator it = frontier.begin(), end = frontier.end();
+    expr_ref_vector ors(m());
+    for (; it != end; ++it) {
+        unsigned_vector states;
+        bool has_final = false;
+        aut->get_epsilon_closure(it->m_key, states);
+        for (unsigned i = 0; i < states.size() && !has_final; ++i) {
+            has_final = aut->is_final_state(states[i]);
+        }
+        if (has_final) {
+            ors.push_back(it->m_value);
+        }
+    }
+    result = mk_or(ors);
+    return BR_REWRITE_FULL;
 }
 br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) {
     return BR_FAILED;
@@ -823,8 +914,7 @@ br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) {
 br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) {
     sort* s;
     VERIFY(m_util.is_re(a, s));
-    sort_ref seq(m_util.str.mk_seq(s), m());
-    result = m_util.re.mk_union(m_util.re.mk_to_re(m_util.str.mk_empty(seq)), a);
+    result = m_util.re.mk_union(m_util.re.mk_to_re(m_util.str.mk_empty(s)), a);
     return BR_REWRITE1;
 }
 
@@ -848,7 +938,6 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
 bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change) {
     expr* a, *b;
     zstring s;
- 
     bool lchange = false;
     SASSERT(lhs.empty());
     // solve from back
@@ -1237,6 +1326,13 @@ bool seq_rewriter::is_subsequence(unsigned szl, expr* const* l, unsigned szr, ex
             found = !rpos.contains(j) && l[i] == r[j];
         }
         if (!found) {
+#if 0
+            std::cout << mk_pp(l[i], m()) << " not found in ";
+            for (unsigned j = 0; j < szr; ++j) {
+                std::cout << mk_pp(r[j], m()) << " ";
+            }
+            std::cout << "\n";
+#endif
             return false;
         }
         SASSERT(0 < j && j <= szr);
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index b9d3460aa..77af42dee 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -26,11 +26,37 @@ Notes:
 #include"lbool.h"
 #include"automaton.h"
 
+class sym_expr {
+    bool     m_is_pred;
+    expr_ref m_t;
+    unsigned m_ref;
+    sym_expr(bool is_pred, expr_ref& t) : m_is_pred(is_pred), m_t(t), 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); }
+    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; }
+    expr* get_char() const { SASSERT(is_char()); return m_t; }
 
-typedef automaton<expr, ast_manager> eautomaton;
+};
+
+class sym_expr_manager {
+public:
+    void inc_ref(sym_expr* s) { if (s) s->inc_ref(); }
+    void dec_ref(sym_expr* s) { if (s) s->dec_ref(); }
+};
+
+typedef automaton<sym_expr, sym_expr_manager> eautomaton;
 class re2automaton {
     ast_manager& m;
-    seq_util     u;       
+    sym_expr_manager sm;
+    seq_util     u;     
+    bv_util      bv;
     eautomaton* re2aut(expr* e);
     eautomaton* seq2aut(expr* e);
  public:
@@ -44,6 +70,7 @@ class re2automaton {
 class seq_rewriter {
     seq_util       m_util;
     arith_util     m_autil;
+    re2automaton   m_re2aut;
     expr_ref_vector m_es, m_lhs, m_rhs;
 
     br_status mk_seq_concat(expr* a, expr* b, expr_ref& result);
@@ -75,11 +102,12 @@ class seq_rewriter {
 
     void add_next(u_map<expr*>& next, unsigned idx, expr* cond);
     bool is_sequence(expr* e, expr_ref_vector& seq);
+    bool is_sequence(eautomaton& aut, expr_ref_vector& seq);
     bool is_epsilon(expr* e) const;
 
 public:    
     seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
-        m_util(m), m_autil(m), m_es(m), m_lhs(m), m_rhs(m) {
+        m_util(m), m_autil(m), m_re2aut(m), m_es(m), m_lhs(m), m_rhs(m) {
     }
     ast_manager & m() const { return m_util.get_manager(); }
     family_id get_fid() const { return m_util.get_family_id(); }
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 165e24eac..66ff7116a 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -22,12 +22,46 @@ Revision History:
 #include "ast_pp.h"
 #include <sstream>
 
+static bool is_hex_digit(char ch, unsigned& d) {
+    if ('0' <= ch && ch <= '9') {
+        d = ch - '0';
+        return true;
+    }
+    if ('A' <= ch && ch <= 'F') {
+        d = 10 + ch - 'A';
+        return true;
+    }
+    return false;
+}
+
+static bool is_escape_char(char const *& s, unsigned& result) {
+    unsigned d1, d2;
+    if (*s == '\\' && *(s + 1) == 'x' && 
+        is_hex_digit(*(s + 2), d1) && is_hex_digit(*(s + 3), d2)) {
+        result = d1*16 + d2;
+        s += 4;
+        return true;
+    }
+    if (*s == '\\' && *(s + 1) == '\\') {
+        result = '\\';
+        s += 2;
+        return true;
+    }
+    return false;
+}
+
 zstring::zstring(encoding enc): m_encoding(enc) {}
 
 zstring::zstring(char const* s, encoding enc): m_encoding(enc) {
     while (*s) {
-        m_buffer.push_back(*s);
-        ++s;
+        unsigned ch;
+        if (is_escape_char(s, ch)) {
+            m_buffer.push_back(ch);
+        }
+        else {            
+            m_buffer.push_back(*s);
+            ++s;
+        }
     }
 }
 
@@ -80,9 +114,10 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const {
     return result;
 }
 
-static const char esc_table[32][3] =
-    { "\\0", "^A", "^B", "^C", "^D", "^E", "^F", "\\a", "\\b", "\\t", "\\n", "\\v", "\\f", "\\r", "^N",
-      "^O", "^P", "^Q", "^R", "^S", "^T", "^U", "^V","^W","^X","^Y","^Z","\\e","^\\","^]","^^","^_"};
+static const char esc_table[32][6] =
+    { "\\x00", "\\x01", "\\x02", "\\x03", "\\x04", "\\x05", "\\x06", "\\x07", "\\x08", "\\x09", "\\n",   "\\v",   "\\f",   "\\r",   "\\x0E", "\\x0F", 
+      "\\x10", "\\x11", "\\x12", "\\x13", "\\x14", "\\x15", "\\x16", "\\x17", "\\x18", "\\x19", "\\x1A", "\\x1B", "\\x1C", "\\x1D", "\\x1E", "\\x1F"
+};
  
 std::string zstring::encode() const {
     SASSERT(m_encoding == ascii);
@@ -91,7 +126,7 @@ std::string zstring::encode() const {
         unsigned char ch = m_buffer[i];
         if (0 <= ch && ch < 32) {
             strm << esc_table[ch];
-        }
+        }        
         else if (ch == 127) {
             strm << "^?";
         }
@@ -250,7 +285,13 @@ void seq_decl_plugin::match_right_assoc(psig& sig, unsigned dsz, sort *const* do
     if (!is_match) {
         std::ostringstream strm;
         strm << "Sort of function '" << sig.m_name << "' ";
-        strm << "does not match the declared type";
+        strm << "does not match the declared type. Given domain: ";
+        for (unsigned i = 0; i < dsz; ++i) {
+            strm << mk_pp(dom[i], m) << " ";
+        }
+        if (range) {
+            strm << " and range: " << mk_pp(range, m);
+        }
         m.raise_exception(strm.str().c_str());
     }
     range_out = apply_binding(binding, sig.m_range);
@@ -277,7 +318,19 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran
     if (!is_match) {
         std::ostringstream strm;
         strm << "Sort of polymorphic function '" << sig.m_name << "' ";
-        strm << "does not match the declared type";
+        strm << "does not match the declared type. ";
+        strm << "\nGiven domain: ";
+        for (unsigned i = 0; i < dsz; ++i) {
+            strm << mk_pp(dom[i], m) << " ";
+        }
+        if (range) {
+            strm << " and range: " << mk_pp(range, m);
+        }
+        strm << "\nExpected domain: ";
+        for (unsigned i = 0; i < dsz; ++i) {
+            strm << mk_pp(sig.m_dom[i].get(), m) << " ";
+        }
+        
         m.raise_exception(strm.str().c_str());
     }
     if (!range && dsz == 0) {
@@ -319,7 +372,8 @@ void seq_decl_plugin::init() {
     parameter paramA(A);
     parameter paramS(strT);
     sort* seqA = m.mk_sort(m_family_id, SEQ_SORT, 1, &paramA);
-    sort* reA  = m.mk_sort(m_family_id, RE_SORT, 1, &paramA);
+    parameter paramSA(seqA);
+    sort* reA  = m.mk_sort(m_family_id, RE_SORT, 1, &paramSA);
     sort* reT  = m.mk_sort(m_family_id, RE_SORT, 1, &paramS);
     sort* boolT = m.mk_bool_sort();
     sort* intT  = arith_util(m).mk_int();
@@ -356,7 +410,7 @@ void seq_decl_plugin::init() {
     m_sigs[OP_RE_CONCAT]     = alloc(psig, m, "re.++",        1, 2, reAreA, reA);
     m_sigs[OP_RE_UNION]      = alloc(psig, m, "re.union",     1, 2, reAreA, reA);
     m_sigs[OP_RE_INTERSECT]  = alloc(psig, m, "re.inter",     1, 2, reAreA, reA);
-    m_sigs[OP_RE_LOOP]           = alloc(psig, m, "re-loop",    1, 1, &reA, reA);
+    m_sigs[OP_RE_LOOP]           = alloc(psig, m, "re.loop",    1, 1, &reA, reA);
     m_sigs[OP_RE_EMPTY_SET]      = alloc(psig, m, "re-empty-set", 1, 0, 0, reA);
     m_sigs[OP_RE_FULL_SET]       = alloc(psig, m, "re-full-set", 1, 0, 0, reA);
     m_sigs[OP_RE_OF_PRED]        = alloc(psig, m, "re-of-pred", 1, 1, &predA, reA);
@@ -367,7 +421,6 @@ void seq_decl_plugin::init() {
     m_sigs[_OP_STRING_STRREPL]   = alloc(psig, m, "str.replace", 0, 3, str3T, strT);
     m_sigs[OP_STRING_ITOS]       = alloc(psig, m, "int.to.str", 0, 1, &intT, strT);
     m_sigs[OP_STRING_STOI]       = alloc(psig, m, "str.to.int", 0, 1, &strT, intT);
-    m_sigs[OP_REGEXP_LOOP]       = alloc(psig, m, "re.loop", 0, 2, strTint2T, reT); // maybe 3 arguments.
     m_sigs[_OP_STRING_CONCAT]    = alloc(psig, m, "str.++", 1, 2, str2T, strT);
     m_sigs[_OP_STRING_LENGTH]    = alloc(psig, m, "str.len", 0, 1, &strT, intT);
     m_sigs[_OP_STRING_STRCTN]    = alloc(psig, m, "str.contains", 0, 2, str2T, boolT);
@@ -411,7 +464,6 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter
         if (!parameters[0].is_ast() || !is_sort(parameters[0].get_ast())) {
             m.raise_exception("invalid regex sort, parameter is not a sort");
         }
-        sort * s = to_sort(parameters[0].get_ast());
         return m.mk_sort(symbol("RegEx"), sort_info(m_family_id, RE_SORT, num_parameters, parameters));
     }
     case _STRING_SORT:
@@ -472,7 +524,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case OP_RE_OF_PRED:
     case OP_STRING_ITOS:
     case OP_STRING_STOI:
-    case OP_REGEXP_LOOP:
         match(*m_sigs[k], arity, domain, range, rng);
         return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
 
@@ -670,3 +721,18 @@ void seq_util::str::get_concat(expr* e, expr_ref_vector& es) const {
         es.push_back(e);
     }
 }
+
+bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi)  {
+    if (is_loop(n)) {
+        app const* a = to_app(n);
+        SASSERT(a->get_num_args() == 1);
+        SASSERT(a->get_decl()->get_num_parameters() == 2);
+        body = a->get_arg(0);
+        lo = a->get_decl()->get_parameter(0).get_int();
+        hi = a->get_decl()->get_parameter(1).get_int();
+        return true;
+    }
+    else {
+        return false;
+    }
+}
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 00ada9e86..e97e92962 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -63,7 +63,6 @@ enum seq_op_kind {
     OP_STRING_CONST,
     OP_STRING_ITOS, 
     OP_STRING_STOI, 
-    OP_REGEXP_LOOP,    // TBD re-loop: integers as parameters or arguments?
     // internal only operators. Converted to SEQ variants.
     _OP_STRING_STRREPL, 
     _OP_STRING_CONCAT, 
@@ -99,6 +98,7 @@ public:
     zstring& operator=(zstring const& other);
     zstring replace(zstring const& src, zstring const& dst) const;
     unsigned num_bits() const { return (m_encoding==ascii)?8:16; }
+    encoding get_encoding() const { return m_encoding; }
     std::string encode() const; 
     unsigned length() const { return m_buffer.size(); }
     unsigned operator[](unsigned i) const { return m_buffer[i]; }
@@ -299,20 +299,23 @@ public:
         bool is_to_re(expr const* n)    const { return is_app_of(n, m_fid, OP_SEQ_TO_RE); }
         bool is_concat(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_CONCAT); }
         bool is_union(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_UNION); }
-        bool is_inter(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_INTERSECT); }
+        bool is_intersection(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_INTERSECT); }
         bool is_star(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_STAR); }
         bool is_plus(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_PLUS); }
         bool is_opt(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_OPTION); }
         bool is_range(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_RANGE); }
-        bool is_loop(expr const* n)    const { return is_app_of(n, m_fid, OP_REGEXP_LOOP); }
-       
+        bool is_loop(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_LOOP); }
+        bool is_empty(expr const* n)  const { return is_app_of(n, m_fid, OP_RE_EMPTY_SET); }
+        bool is_full(expr const* n)  const { return is_app_of(n, m_fid, OP_RE_FULL_SET); }
         MATCH_UNARY(is_to_re);
         MATCH_BINARY(is_concat);
         MATCH_BINARY(is_union);
-        MATCH_BINARY(is_inter);
+        MATCH_BINARY(is_intersection);
+        MATCH_BINARY(is_range);
         MATCH_UNARY(is_star);
         MATCH_UNARY(is_plus);
         MATCH_UNARY(is_opt);
+        bool is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi);
         
     };
     str str;
diff --git a/src/math/automata/automaton.h b/src/math/automata/automaton.h
index e7d7c8bfb..084f3e4f8 100644
--- a/src/math/automata/automaton.h
+++ b/src/math/automata/automaton.h
@@ -151,7 +151,7 @@ public:
         m_final_states(other.m_final_states)
     {}
 
-    // create the automaton that accepts the empty string only.
+    // create the automaton that accepts the empty string/sequence only.
     static automaton* mk_epsilon(M& m) {
         moves mvs;
         unsigned_vector final;
@@ -168,10 +168,24 @@ public:
         return alloc(automaton, m, 0, final, mvs);
     }
 
+    static automaton* clone(automaton const& a) {
+        moves mvs;
+        unsigned_vector final;
+        append_moves(0, a, mvs);
+        append_final(0, a, final);
+        return alloc(automaton, a.m, a.init(), final, mvs);
+    }
+
     // create the sum of disjoint automata
     static automaton* mk_union(automaton const& a, automaton const& b) {
         SASSERT(&a.m == &b.m);
         M& m = a.m;
+        if (a.is_empty()) {
+            return clone(b);
+        }
+        if (b.is_empty()) {
+            return clone(a);
+        }
         moves mvs;
         unsigned_vector final;
         unsigned offset1 = 1;
@@ -196,6 +210,10 @@ public:
             init = 0;
             mvs.push_back(move(m, 0, a.init() + offset));
         }
+        if (a.is_empty()) {
+            return clone(a);
+        }
+
         mvs.push_back(move(m, init, a.final_state() + offset));
         append_moves(offset, a, mvs);
         append_final(offset, a, final);
@@ -206,6 +224,19 @@ public:
     static automaton* mk_concat(automaton const& a, automaton const& b) {
         SASSERT(&a.m == &b.m);
         M& m = a.m;
+        if (a.is_empty()) {
+            return clone(a);
+        }
+        if (b.is_empty()) {
+            return clone(b);
+        }
+        if (a.is_epsilon()) {
+            return clone(b);
+        }
+        if (b.is_epsilon()) {
+            return clone(a);
+        }
+
         moves mvs;
         unsigned_vector final;
         unsigned init = 0;
@@ -295,6 +326,10 @@ public:
     // 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
     // 
+    // Some missing: 
+    //  src - et -> dst - E -> Dst1 => src - et -> Dst1   if in_degree(dst) = 1
+    //  Src - ET -> dst - e -> dst1 => Src - ET -> dst1  if out_degree(dst) = 1, 
+    //
     void compress() {
         for (unsigned i = 0; i < m_delta.size(); ++i) {
             for (unsigned j = 0; j < m_delta[i].size(); ++j) {
@@ -446,6 +481,7 @@ public:
     }
 
     bool is_empty() const { return m_final_states.empty(); }
+    bool is_epsilon() const { return m_final_states.size() == 1 && m_final_states.back() == init() && m_delta.empty(); }
     unsigned final_state() const { return m_final_states[0]; }
     bool has_single_final_sink() const { return m_final_states.size() == 1 && m_delta[final_state()].empty(); }
     unsigned num_states() const { return m_delta.size(); }
diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp
index fb594a09f..90810f294 100644
--- a/src/model/func_interp.cpp
+++ b/src/model/func_interp.cpp
@@ -169,6 +169,7 @@ void func_interp::insert_new_entry(expr * const * args, expr * r) {
            for (unsigned i = 0; i < m_arity; i++) {
                tout << mk_ismt2_pp(args[i], m_manager) << "\n";
            }
+           tout << "Old: " << mk_ismt2_pp(get_entry(args)->get_result(), m_manager) << "\n";
            );
     SASSERT(get_entry(args) == 0);
     func_entry * new_entry = func_entry::mk(m_manager, m_arity, args, r);
diff --git a/src/muz/base/dl_engine_base.h b/src/muz/base/dl_engine_base.h
index e0d8680b2..f353fbf2e 100644
--- a/src/muz/base/dl_engine_base.h
+++ b/src/muz/base/dl_engine_base.h
@@ -44,7 +44,26 @@ namespace datalog {
 
         virtual expr_ref get_answer() = 0;
         virtual lbool query(expr* q) = 0;
-        virtual lbool query(unsigned num_rels, func_decl*const* rels) { return l_undef; }
+        virtual lbool query(unsigned num_rels, func_decl*const* rels) { 
+            if (num_rels != 1) return l_undef;
+            expr_ref q(m);
+            expr_ref_vector args(m);
+            sort_ref_vector sorts(m);
+            svector<symbol> names;
+            func_decl* r = rels[0];
+            for (unsigned i = 0; i < r->get_arity(); ++i) {
+                args.push_back(m.mk_var(i, r->get_domain(i)));
+                sorts.push_back(r->get_domain(i));
+                names.push_back(symbol(i));
+            }
+            sorts.reverse();
+            names.reverse();
+            q = m.mk_app(r, args.size(), args.c_ptr());
+            if (!args.empty()) {
+                q = m.mk_exists(sorts.size(), sorts.c_ptr(), names.c_ptr(), q);
+            }
+            return query(q);
+        }
 
         virtual void reset_statistics() {}
         virtual void display_profile(std::ostream& out) const {}
diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp
index f8e97d95d..2a6ff04d4 100644
--- a/src/muz/fp/dl_cmds.cpp
+++ b/src/muz/fp/dl_cmds.cpp
@@ -268,10 +268,10 @@ public:
             print_certificate(ctx);
             break;
         case l_undef: 
-            if(dlctx.get_status() == datalog::BOUNDED){
-              ctx.regular_stream() << "bounded\n";
-              print_certificate(ctx);
-              break;
+            if (dlctx.get_status() == datalog::BOUNDED){
+                ctx.regular_stream() << "bounded\n";
+                print_certificate(ctx);
+                break;
             }
             ctx.regular_stream() << "unknown\n";
             switch(dlctx.get_status()) {
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index b6350ed28..f23207f66 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -399,7 +399,7 @@ namespace smt2 {
         void check_keyword(char const * msg) { if (!curr_is_keyword()) throw parser_exception(msg); }
         void check_string(char const * msg) { if (!curr_is_string()) throw parser_exception(msg); }
         void check_int(char const * msg) { if (!curr_is_int()) throw parser_exception(msg); }
-        void check_int_or_float(char const * msg) { if (!curr_is_int() || !curr_is_float()) throw parser_exception(msg); }
+        void check_int_or_float(char const * msg) { if (!curr_is_int() && !curr_is_float()) throw parser_exception(msg); }
         void check_float(char const * msg) { if (!curr_is_float()) throw parser_exception(msg); }
 
         void error(unsigned line, unsigned pos, char const * msg) {
@@ -2341,7 +2341,7 @@ namespace smt2 {
                 break;
             }
             case CPK_NUMERAL:
-                check_int("invalid command argument, numeral expected");
+                check_int_or_float("invalid command argument, numeral expected");
                 m_curr_cmd->set_next_arg(m_ctx, curr_numeral());
                 next();
                 break;
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index 703e19f1d..8ccee885a 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -547,6 +547,7 @@ namespace smt {
         ptr_vector<expr> m_todo;
         bool is_int_expr(expr* e);
         bool is_int(theory_var v) const { return m_data[v].m_is_int; }
+        bool is_int_src(theory_var v) const { return m_util.is_int(var2expr(v)); }
         bool is_real(theory_var v) const { return !is_int(v); }
         bool get_implied_old_value(theory_var v, inf_numeral & r) const;
         inf_numeral const & get_implied_value(theory_var v) const;
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 6f245d1c6..1b1b9a1a6 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -66,6 +66,9 @@ namespace smt {
 
     template<typename Ext>
     bool theory_arith<Ext>::is_int_expr(expr* e) {
+#if 0
+        return m_util.is_int(e);
+#else
         if (m_util.is_int(e)) return true;
         if (is_uninterp(e)) return false;
         m_todo.reset();
@@ -93,6 +96,7 @@ namespace smt {
             }
         }
         return true;
+#endif
     }
 
 
@@ -3073,7 +3077,7 @@ namespace smt {
             theory_var num = get_num_vars();
             bool refine = false;
             for (theory_var v = 0; v < num; v++) {
-                if (is_int(v))
+                if (is_int_src(v))
                     continue;
                 if (!get_context().is_shared(get_enode(v)))
                     continue;
@@ -3084,7 +3088,7 @@ namespace smt {
                 rational value = val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational();
                 theory_var v2;
                 if (mapping.find(value, v2)) {
-                    SASSERT(!is_int(v2));
+                    SASSERT(!is_int_src(v2));
                     if (get_value(v) != get_value(v2)) {
                         // v and v2 are not known to be equal. 
                         // The choice of m_epsilon is making them equal.
@@ -3126,7 +3130,7 @@ namespace smt {
             TRACE("arith", tout << "Truncating non-integer value. This is possible for non-linear constraints v" << v << " " << num << "\n";);
             num = floor(num);
         }
-        return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int(v)));
+        return alloc(expr_wrapper_proc, m_factory->mk_value(num, m_util.is_int(var2expr(v))));
     }
 
     // -----------------------------------
diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h
index 7ed6cfe50..8e1b52ee5 100644
--- a/src/smt/theory_arith_eq.h
+++ b/src/smt/theory_arith_eq.h
@@ -43,7 +43,7 @@ namespace smt {
         CTRACE("arith_bug", !lower_bound(v).is_rational(), display_var(tout, v););
         SASSERT(lower_bound(v).is_rational());
         numeral const & val = lower_bound(v).get_rational();
-        value_sort_pair key(val, is_int(v));
+        value_sort_pair key(val, is_int_src(v));
         theory_var v2;
         if (m_fixed_var_table.find(key, v2)) {
             if (v2 < static_cast<int>(get_num_vars()) && is_fixed(v2) && lower_bound(v2).get_rational() == val) {
@@ -51,7 +51,7 @@ namespace smt {
                 // The table m_fixed_var_table is not restored during backtrack. So, it may
                 // contain invalid (key -> value) pairs. So, we must check whether v2 is really equal to val (previous test) AND it has
                 // the same sort of v. The following test was missing in a previous version of Z3. 
-                if (!is_equal(v, v2) && is_int(v) == is_int(v2)) {
+                if (!is_equal(v, v2) && is_int_src(v) == is_int_src(v2)) {
                     antecedents ante(*this);
 
                     //
@@ -226,7 +226,7 @@ namespace smt {
             
             if (y == null_theory_var) {
                 // x is an implied fixed var at k.
-                value_sort_pair key(k, is_int(x));
+                value_sort_pair key(k, is_int_src(x));
                 theory_var x2;
                 if (m_fixed_var_table.find(key, x2) && 
                     x2 < static_cast<int>(get_num_vars()) && 
@@ -238,7 +238,7 @@ namespace smt {
                     // So, we must check whether x2 is really equal to k (previous test) 
                     // AND has the same sort of x.
                     // The following test was missing in a previous version of Z3. 
-                    is_int(x) == is_int(x2) &&
+                    is_int_src(x) == is_int_src(x2) &&
                     !is_equal(x, x2)) {
 
                     antecedents ante(*this);
@@ -254,7 +254,7 @@ namespace smt {
                 }
             }
 
-            if (k.is_zero() && y != null_theory_var && !is_equal(x, y) && is_int(x) == is_int(y)) {
+            if (k.is_zero() && y != null_theory_var && !is_equal(x, y) && is_int_src(x) == is_int_src(y)) {
                 // found equality x = y
                 antecedents ante(*this);
                 collect_fixed_var_justifications(r, ante);
@@ -294,7 +294,7 @@ namespace smt {
                     }
 
                     if (new_eq) {
-                        if (!is_equal(x, x2) && is_int(x) == is_int(x2)) {
+                        if (!is_equal(x, x2) && is_int_src(x) == is_int_src(x2)) {
                             SASSERT(y == y2 && k == k2);
                             antecedents ante(*this);
                             collect_fixed_var_justifications(r, ante);
@@ -323,12 +323,12 @@ namespace smt {
 
     template<typename Ext>
     void theory_arith<Ext>::propagate_eq_to_core(theory_var x, theory_var y, antecedents& antecedents) {
-        // I doesn't make sense to propagate an equality (to the core) of variables of different sort.
-        SASSERT(is_int(x) == is_int(y));
         // Ignore equality if variables are already known to be equal.
         if (is_equal(x, y))
             return;
+        // I doesn't make sense to propagate an equality (to the core) of variables of different sort.
         if (get_manager().get_sort(var2expr(x)) != get_manager().get_sort(var2expr(y))) {
+            TRACE("arith", tout << mk_pp(var2expr(x), get_manager()) << " = " << mk_pp(var2expr(y), get_manager()) << "\n";);
             return;
         }
         context & ctx      = get_context();
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index c1083ea25..c7fab3934 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -31,8 +31,8 @@ using namespace smt;
 struct display_expr {
     ast_manager& m;
     display_expr(ast_manager& m): m(m) {}
-    std::ostream& display(std::ostream& out, expr* e) const {
-        return out << mk_pp(e, m);
+    std::ostream& display(std::ostream& out, sym_expr* e) const {
+        return e->display(out);
     }
 };
 
@@ -165,11 +165,12 @@ theory_seq::theory_seq(ast_manager& m):
     m_util(m),
     m_autil(m),
     m_trail_stack(*this),
-    m_atoms_qhead(0),
     m_ls(m), m_rs(m),
     m_lhs(m), m_rhs(m),
+    m_atoms_qhead(0),
     m_new_solution(false),
-    m_new_propagation(false) {    
+    m_new_propagation(false),
+    m_mk_aut(m) {    
     m_prefix = "seq.prefix.suffix";
     m_suffix = "seq.suffix.prefix";
     m_contains_left = "seq.contains.left";
@@ -194,7 +195,6 @@ theory_seq::~theory_seq() {
 
 
 final_check_status theory_seq::final_check_eh() { 
-    context & ctx   = get_context();
     TRACE("seq", display(tout););
     if (simplify_and_solve_eqs()) {
         ++m_stats.m_solve_eqs;
@@ -760,7 +760,6 @@ bool theory_seq::add_solution(expr* l, expr* r, dependency* deps)  {
     if (l == r) {
         return false;
     }
-    context& ctx = get_context();
     TRACE("seq", tout << mk_pp(l, m) << " ==> " << mk_pp(r, m) << "\n";);
     m_new_solution = true;
     m_rep.update(l, r, deps);
@@ -933,7 +932,6 @@ bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector cons
 }
 
 bool theory_seq::solve_nqs(unsigned i) {
-    bool change = false;
     context & ctx = get_context();
     for (; !ctx.inconsistent() && i < m_nqs.size(); ++i) {
         if (solve_ne(i)) {
@@ -1179,7 +1177,9 @@ void theory_seq::display(std::ostream & out) const {
         for (; it != end; ++it) {
             out << mk_pp(it->m_key, m) << "\n";
             display_expr disp(m);
-            it->m_value->display(out, disp);
+            if (it->m_value) {
+                it->m_value->display(out, disp);
+            }
         }
     }
     if (!m_rep.empty()) {
@@ -1262,7 +1262,7 @@ void theory_seq::init_model(expr_ref_vector const& es) {
 }
 
 void theory_seq::init_model(model_generator & mg) {
-    m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model());
+    m_factory = alloc(seq_factory, get_manager(), get_family_id());
     mg.register_factory(m_factory);
     for (unsigned j = 0; j < m_nqs.size(); ++j) {
         ne const& n = m_nqs[j];
@@ -1288,7 +1288,6 @@ public:
     }
     virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values) {
         SASSERT(values.size() == m_dependencies.size());
-        ast_manager& m = mg.get_manager();
         if (values.empty()) {
             return th.mk_value(n);
         }
@@ -1326,7 +1325,10 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
     
     if (concats.size() > 1) {
         for (unsigned i = 0; i < concats.size(); ++i) {
-            sv->add_dependency(ctx.get_enode(concats[i]));
+            expr* e = concats[i];
+            if (!m_util.str.is_string(e)) {
+                sv->add_dependency(ctx.get_enode(e));
+            }
         }
     }
     else if (m_util.str.is_unit(e, e1)) {
@@ -1362,7 +1364,8 @@ app* theory_seq::mk_value(app* e) {
         unsigned sz;
         if (bv.is_numeral(result, val, sz) && sz == zstring().num_bits()) {
             unsigned v = val.get_unsigned();
-            if ((0 <= v && v < 7) || (14 <= v && v < 32) || v == 127) {
+            if (false && ((v < 7) || (14 <= v && v < 32) || v == 127)) {
+                // disabled: use escape characters.
                 result = m_util.str.mk_unit(result);                
             }
             else {
@@ -1817,7 +1820,6 @@ enode* theory_seq::ensure_enode(expr* e) {
 }
 
 static theory_mi_arith* get_th_arith(context& ctx, theory_id afid, expr* e) {
-    ast_manager& m = ctx.get_manager();
     theory* th = ctx.get_theory(afid);
     if (th && ctx.e_internalized(e)) {
         return dynamic_cast<theory_mi_arith*>(th);
@@ -1957,11 +1959,10 @@ void theory_seq::add_at_axiom(expr* e) {
 void theory_seq::propagate_step(literal lit, expr* step) {
     context& ctx = get_context();
     SASSERT(ctx.get_assignment(lit) == l_true);
-    expr* re, *t, *s, *idx, *i, *j;
-    VERIFY(is_step(step, s, idx, re, i, j, t));
-    expr_ref nth = mk_nth(s, idx);
-    TRACE("seq", tout << mk_pp(step, m) << " -> " << mk_pp(t, m) << " = " << nth << "\n";);
-    propagate_eq(lit, t, nth);
+    expr* re, *acc, *s, *idx, *i, *j;
+    VERIFY(is_step(step, s, idx, re, i, j, acc));
+    TRACE("seq", tout << mk_pp(step, m) << " -> " << mk_pp(acc, m) << "\n";);
+    propagate_lit(0, 1, &lit, mk_literal(acc));
     rational lo;
     rational _idx;
     if (lower_bound(s, lo) && lo.is_unsigned() && m_autil.is_numeral(idx, _idx) && lo >= _idx) {
@@ -2255,15 +2256,14 @@ eautomaton* theory_seq::get_automaton(expr* re) {
     if (m_re2aut.find(re, result)) {
         return result;
     }
-    result = re2automaton(m)(re);
+    result = m_mk_aut(re);
     if (result) {
         display_expr disp(m);
         TRACE("seq", result->display(tout, disp););
     }
-    if (result) {
-        m_automata.push_back(result);
-        m_trail_stack.push(push_back_vector<theory_seq, scoped_ptr_vector<eautomaton> >(m_automata));
-    }
+    m_automata.push_back(result);
+    m_trail_stack.push(push_back_vector<theory_seq, scoped_ptr_vector<eautomaton> >(m_automata));
+    
     m_re2aut.insert(re, result);
     m_trail_stack.push(insert_obj_map<theory_seq, expr, eautomaton*>(m_re2aut, re));
     return result;
@@ -2286,10 +2286,11 @@ bool theory_seq::is_acc_rej(symbol const& ar, expr* e, expr*& s, expr*& idx, exp
         s  = to_app(e)->get_arg(0);
         idx = to_app(e)->get_arg(1);
         re = to_app(e)->get_arg(2);
+        TRACE("seq", tout << mk_pp(re, m) << "\n";);
         VERIFY(m_autil.is_numeral(to_app(e)->get_arg(3), r));
         SASSERT(r.is_unsigned());
         i = r.get_unsigned();
-        aut = m_re2aut[re];
+        aut = get_automaton(re);        
         return true;
     }
     else {
@@ -2316,12 +2317,13 @@ bool theory_seq::is_step(expr* e, expr*& s, expr*& idx, expr*& re, expr*& i, exp
     }
 }
 
-expr_ref theory_seq::mk_step(expr* s, expr* idx, expr* re, unsigned i, unsigned j, expr* t) { 
+expr_ref theory_seq::mk_step(expr* s, expr* idx, expr* re, unsigned i, unsigned j, expr* acc) { 
+    SASSERT(m.is_bool(acc));
     expr_ref_vector args(m);
     args.push_back(s).push_back(idx).push_back(re);
     args.push_back(m_autil.mk_int(i));
     args.push_back(m_autil.mk_int(j));
-    args.push_back(t);
+    args.push_back(acc);
     return expr_ref(m_util.mk_skolem(m_aut_step, args.size(), args.c_ptr(), m.mk_bool_sort()), m);
 }
 
@@ -2395,7 +2397,9 @@ bool theory_seq::add_accept2step(expr* acc) {
     for (unsigned i = 0; i < mvs.size(); ++i) {
         unsigned j = (i + start) % mvs.size();
         eautomaton::move mv = mvs[j];
-        step = mk_step(e, idx, re, src, mv.dst(), mv.t());
+        expr_ref nth = mk_nth(e, idx);
+        expr_ref acc = mv.t()->accept(nth);
+        step = mk_step(e, idx, re, src, mv.dst(), acc);
         lits.push_back(mk_literal(step));
         switch (ctx.get_assignment(lits.back())) {
         case l_true:
@@ -2438,8 +2442,8 @@ bool theory_seq::add_accept2step(expr* acc) {
 bool theory_seq::add_step2accept(expr* step) {
     context& ctx = get_context();
     SASSERT(ctx.get_assignment(step) == l_true);
-    expr* re, *t, *s, *idx, *i, *j;
-    VERIFY(is_step(step, s, idx, re, i, j, t));
+    expr* re, *_acc, *s, *idx, *i, *j;
+    VERIFY(is_step(step, s, idx, re, i, j, _acc));
     literal acc1 = mk_accept(s, idx,  re, i);
     switch (ctx.get_assignment(acc1)) {
     case l_false:
@@ -2513,7 +2517,7 @@ bool theory_seq::add_reject2reject(expr* rej) {
     bool has_undef = false;
     for (unsigned i = 0; i < mvs.size(); ++i) {
         eautomaton::move const& mv = mvs[i];        
-        literal eq = mk_eq(nth, mv.t(), false);
+        literal eq = mk_literal(mv.t()->accept(nth)); 
         switch (ctx.get_assignment(eq)) {
         case l_false:
         case l_true:
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 927cec537..8e0b8e17e 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -278,6 +278,7 @@ namespace smt {
         unsigned                       m_atoms_qhead;
         bool                           m_new_solution;     // new solution added
         bool                           m_new_propagation;  // new propagation to core
+        re2automaton                   m_mk_aut;
 
         virtual final_check_status final_check_eh();
         virtual bool internalize_atom(app* atom, bool) { return internalize_term(atom); }
@@ -411,7 +412,7 @@ namespace smt {
             return is_acc_rej(m_reject, rej, s, idx, re, i, aut);
         }
         bool is_acc_rej(symbol const& ar, expr* e, expr*& s, expr*& idx, expr*& re, unsigned& i, eautomaton*& aut);
-        expr_ref mk_step(expr* s, expr* tail, expr* re, unsigned i, unsigned j, expr* t);
+        expr_ref mk_step(expr* s, expr* tail, expr* re, unsigned i, unsigned j, expr* acc);
         bool is_step(expr* e, expr*& s, expr*& tail, expr*& re, expr*& i, expr*& j, expr*& t) const;
         bool is_step(expr* e) const;
         void propagate_step(literal lit, expr* n);
diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h
index 9c8f15a7a..69f8b54b7 100644
--- a/src/smt/theory_seq_empty.h
+++ b/src/smt/theory_seq_empty.h
@@ -26,23 +26,19 @@ namespace smt {
     class seq_factory : public value_factory {
         typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> symbol_set;
         ast_manager& m;
-        proto_model& m_model;
         seq_util     u;
         symbol_set   m_strings;
         unsigned     m_next;
-        char         m_char;
         std::string  m_unique_delim;
         obj_map<sort, expr*> m_unique_sequences;
         expr_ref_vector m_trail;
     public:
 
-        seq_factory(ast_manager & m, family_id fid, proto_model & md):
+        seq_factory(ast_manager & m, family_id fid):
             value_factory(m, fid),
             m(m),
-            m_model(md),
             u(m),
             m_next(0),
-            m_char(0),
             m_unique_delim("!"),
             m_trail(m)
         {
@@ -129,7 +125,7 @@ namespace smt {
     public:
         theory_seq_empty(ast_manager& m):theory(m.mk_family_id("seq")), m_used(false) {}
         virtual void init_model(model_generator & mg) {
-            mg.register_factory(alloc(seq_factory, get_manager(), get_family_id(), mg.get_model()));
+            mg.register_factory(alloc(seq_factory, get_manager(), get_family_id()));
         }
 
     };
diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp
index 24aa253a4..899b8635b 100644
--- a/src/util/mpf.cpp
+++ b/src/util/mpf.cpp
@@ -245,26 +245,30 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode
         m_mpz_manager.set(exp, exponent);
 
         // Normalize such that 1.0 <= sig < 2.0
-        if (m_mpq_manager.ge(sig, mpq(2))) {
+        if (m_mpq_manager.lt(sig, 1)) {
+            m_mpq_manager.inv(sig);
+            unsigned int pp = m_mpq_manager.prev_power_of_two(sig);
+            if (!m_mpq_manager.is_power_of_two(sig, pp)) pp++;
+            scoped_mpz p2(m_mpz_manager);
+            m_mpq_manager.power(2, pp, p2);
+            m_mpq_manager.div(sig, p2, sig);
+            m_mpz_manager.sub(exp, mpz(pp), exp);
+            m_mpq_manager.inv(sig);
+        }
+        else if (m_mpq_manager.ge(sig, 2)) {
             unsigned int pp = m_mpq_manager.prev_power_of_two(sig);
             scoped_mpz p2(m_mpz_manager);
             m_mpq_manager.power(2, pp, p2);
             m_mpq_manager.div(sig, p2, sig);
             m_mpz_manager.add(exp, mpz(pp), exp);
         }
-        SASSERT(m_mpq_manager.lt(sig, mpq(2)));
-
-        while (m_mpq_manager.lt(sig, 1)) {
-            m_mpq_manager.mul(sig, 2, sig);
-            m_mpz_manager.dec(exp);
-        }
-
-        // Check that 1.0 <= sig < 2.0
-        SASSERT((m_mpq_manager.le(1, sig) && m_mpq_manager.lt(sig, 2)));
 
         TRACE("mpf_dbg", tout << "Normalized: sig = " << m_mpq_manager.to_string(sig) <<
                                  " exp = " << m_mpz_manager.to_string(exp) << std::endl;);
 
+        // Check that 1.0 <= sig < 2.0
+        SASSERT((m_mpq_manager.le(1, sig) && m_mpq_manager.lt(sig, 2)));
+
         scoped_mpz p(m_mpq_manager);
         scoped_mpq t(m_mpq_manager), sq(m_mpq_manager);
         m_mpz_manager.power(2, sbits + 3 - 1, p);