CVC4 equivalent of Z3's seq.unit

I'm trying to run the following unsat example with both Z3 and CVC4. If I replace "\x00" with (seq.unit #x00) then it's not a problem for Z3, but CVC4 complains it doesn't know seq.unit.

(declare-fun AB_serial_1_version_0 () String)
(declare-fun AB_serial_1_version_1 () String)

(assert (= (str.len AB_serial_1_version_0) 16))
(assert (= (str.len AB_serial_1_version_1) (str.len AB_serial_1_version_0)))
(assert (= (str.at AB_serial_1_version_1 15) "\x00"))
;;; (assert (= (str.at AB_serial_1_version_1 15) (seq.unit #x00)))

(assert (= (str.indexof (str.substr AB_serial_1_version_1 0 (- 16 0)) "\x00" 0) (- 0 1)))
(check-sat)

Here is the command line call:

cvc4 --strings-exp --quiet --produce-models --lang=smt2 ./example.txt

And here is what cvc4 complains about when I use the seq.unit line instead:

(error "Parse Error: ./example.txt:7.54: Symbol 'seq.unit' not declared as a variable

...= (str.at AB_serial_1_version_1 15) (seq.unit #x00)))
                                        ^
")

Solution

This is the answer from CVC4/issues (brought here for completeness):

Thanks for the benchmark. Unfortunately there isn't anything that converts between bitvectors and strings at the moment.

We are planning to add support for sequences soon (issue #1122). Although of course there isn't an SMT standard for sequences yet. I will keep this issue in mind when we add support for sequences.