smt - Z3のseq.unitに相当するCVC4

Question

Z3 と CVC4 の両方で次の unsat の例を実行しようとしています。"\x00"を(seq.unit #x00)に置き換えれば、Z3 では問題ありませんが、CVC4 では 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)

コマンドライン呼び出しは次のとおりです。

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

そして、代わりに seq.unit 行を使用したときにcvc4が不満を言うのは次のとおりです。

(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)))
                                        ^
")