Support for constant arrays

[blishko]

Hi!

It seems that Yices does not support constant arrays, is that correct?

(set-logic QF_ABV)
(define-sort Byte () (_ BitVec 8))
(define-sort Word () (_ BitVec 256))
(define-sort Buf () (Array Word Byte))
(declare-fun x () Buf)
(assert (= x ((as const Buf) #b00000000)))
(check-sat)

(error "at line 6, column 19: undefined term: const")

Do you plan to support constant arrays in Yices?

[disteph]

Yes, though not in the next release 2.8. Let's table this for 2.8.1.