diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 67c0b5975..df0830150 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -3498,8 +3498,8 @@ namespace seq {
             VERIFY(m_seq.is_re(stabilizer_re->get_expr(), seq_sort));
 
             // Construct the replacement x = x' x''
-            euf::snode* xp      = mk_fresh_var(x->get_sort());
-            euf::snode* xpp     = mk_fresh_var(x->get_sort());
+            euf::snode* xp      = m_sg.mk(m_sk.mk("cycle", x->get_expr(), stabilizer_re->get_expr(), seq_sort));
+            euf::snode* xpp     = get_tail(x, compute_length_expr(xp).get());
             euf::snode* xp_xpp  = m_sg.mk_concat(xp, xpp);
 
             nielsen_node* child = mk_child(node);
diff --git a/src/smt/seq_model.cpp b/src/smt/seq_model.cpp
index 371bb782a..a676f0cd2 100644
--- a/src/smt/seq_model.cpp
+++ b/src/smt/seq_model.cpp
@@ -460,7 +460,8 @@ namespace smt {
             expr_ref witness(m);
             // We checked non-emptiness during Nielsen already
             lbool wr = m_rewriter.some_seq_in_re(re_expr, witness);
-            if (wr == l_true && witness) {
+            if (wr == l_true) {
+                SASSERT(witness);
                 m_trail.push_back(witness);
                 m_factory->register_value(witness);
                 return witness;