How to convert numeric character to Unicode string?

[johannes-collab]

With the old sequence solver, we used seq.unit to convert characters to strings.

(declare-const str String)
(assert (= str (seq.unit #x61)))

This doesn't seem to be possible with the Unicode string solver (the new default). Am I missing something here?

[krobelus]

Nevermind, it's str.from_code, as per http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml