diff --git a/src/smt/seq_unicode.cpp b/src/smt/seq_unicode.cpp
index 65ec93277..2a10369e4 100644
--- a/src/smt/seq_unicode.cpp
+++ b/src/smt/seq_unicode.cpp
@@ -89,7 +89,7 @@ namespace smt {
             for (literal bit : bits)
                 ctx().mark_as_relevant(bit);
             expr_ref bits2char(seq.mk_skolem(m_bits2char, ebits.size(), ebits.c_ptr(), m.get_sort(e)), m);
-            ctx().mark_as_relevant(bits2char);
+            ctx().mark_as_relevant(bits2char.get());
             enode* n1 = th.ensure_enode(e);
             enode* n2 = th.ensure_enode(bits2char);
             justification* j =