Я пытаюсь запустить следующий пример unsat как с Z3, так и с CVC4. Если я заменю "\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
И вот на что жалуется cvc4, когда я вместо этого использую строку seq.unit:
(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)))
^
")
