diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index f06afce71..c1083ea25 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -551,9 +551,6 @@ bool theory_seq::is_solved() {
         IF_VERBOSE(10, verbose_stream() << "(seq.giveup " << m_eqs[0].ls() << " = " << m_eqs[0].rs() << " is unsolved)\n";);
         return false;
     }
-    if (!m_nqs.empty()) {
-        return false;
-    }
     for (unsigned i = 0; i < m_automata.size(); ++i) {
         if (!m_automata[i]) {
             IF_VERBOSE(10, verbose_stream() << "(seq.giveup regular expression did not compile to automaton)\n";);
@@ -1252,9 +1249,28 @@ void theory_seq::collect_statistics(::statistics & st) const {
     st.update("seq add axiom", m_stats.m_add_axiom);
 }
 
+void theory_seq::init_model(expr_ref_vector const& es) {
+    expr_ref new_s(m);
+    for (unsigned i = 0; i < es.size(); ++i) {
+        dependency* eqs = 0;
+        expr_ref s = canonize(es[i], eqs);
+        if (is_var(s)) {
+            new_s = m_factory->get_fresh_value(m.get_sort(s));
+            m_rep.update(s, new_s, eqs);
+        }
+    }
+}
+
 void theory_seq::init_model(model_generator & mg) {
     m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model());
     mg.register_factory(m_factory);
+    for (unsigned j = 0; j < m_nqs.size(); ++j) {
+        ne const& n = m_nqs[j];
+        for (unsigned i = 0; i < n.ls().size(); ++i) {
+            init_model(n.ls(i));
+            init_model(n.rs(i));
+        }
+    }
 }
 
 
@@ -2182,7 +2198,7 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
     m_rewrite(eq);
     if (!m.is_false(eq)) {
         literal lit = ~mk_eq(e1, e2, false);
-        SASSERT(get_context().get_assignment(lit) == l_true);
+        //SASSERT(get_context().get_assignment(lit) == l_true);
         dependency* dep = m_dm.mk_leaf(assumption(lit));
         m_nqs.push_back(ne(e1, e2, dep));
         solve_nqs(m_nqs.size() - 1);
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index d14dbba6d..927cec537 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -301,6 +301,7 @@ namespace smt {
         virtual model_value_proc * mk_value(enode * n, model_generator & mg);
         virtual void init_model(model_generator & mg);
 
+        void init_model(expr_ref_vector const& es);
         // final check 
         bool simplify_and_solve_eqs();   // solve unitary equalities
         bool branch_variable();          // branch on a variable
diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h
index 5065c733d..9c8f15a7a 100644
--- a/src/smt/theory_seq_empty.h
+++ b/src/smt/theory_seq_empty.h
@@ -31,7 +31,7 @@ namespace smt {
         symbol_set   m_strings;
         unsigned     m_next;
         char         m_char;
-        std::string  m_unique_prefix;
+        std::string  m_unique_delim;
         obj_map<sort, expr*> m_unique_sequences;
         expr_ref_vector m_trail;
     public:
@@ -43,7 +43,7 @@ namespace smt {
             u(m),
             m_next(0),
             m_char(0),
-            m_unique_prefix("#B"),
+            m_unique_delim("!"),
             m_trail(m)
         {
             m_strings.insert(symbol(""));
@@ -56,7 +56,7 @@ namespace smt {
         }
 
         void set_prefix(char const* p) {
-            m_unique_prefix = p;
+            m_unique_delim = p;
         }
 
         // generic method for setting unique sequences
@@ -89,7 +89,7 @@ namespace smt {
             if (u.is_string(s)) {
                 while (true) {
                     std::ostringstream strm;
-                    strm << m_unique_prefix << m_next++;
+                    strm << m_unique_delim << std::hex << m_next++ << std::dec << m_unique_delim;
                     symbol sym(strm.str().c_str());
                     if (m_strings.contains(sym)) continue;
                     m_strings.insert(sym);