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