yices2
yices2 copied to clipboard
Support for constant arrays
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?