yices2 icon indicating copy to clipboard operation
yices2 copied to clipboard

Support for constant arrays

Open blishko opened this issue 6 months ago • 0 comments

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?

blishko avatar Jul 18 '25 15:07 blishko