As far as I know, there are three ways to assgin values to an array in z3.
assert
to assgin values to some of the cells:(declare-const a1 (Array Int Int))
(declare-const a2 (Array Int Int))
(assert (= 1 (select a1 0)))
(assert (= 2 (select a2 0)))
z3 returns unsat
when the constraint (assert (= a1 a2))
is added.
as const
to initialize the array first and then assgin values to specific cells:(declare-const a3 (Array Int Int))
(assert
(=
(store ((as const (Array Int Int)) 64) 0 3)
a3
)
)
(declare-const a4 (Array Int Int))
(assert
(=
(store ((as const (Array Int Int)) 64) 0 4)
a4
)
)
Add (assert (= a3 a4))
and we obtain unsat
again.
(define-const a5 (Array Int Int)
(lambda ((i Int))
(ite (= i 0) 5 64)))
(define-const a6 (Array Int Int)
(lambda ((i Int))
(ite (= i 0) 6 64)))
But if we add (assert (= a5 a6))
, z3 returns sat
. Why?
By the way, is there any (better) way to assign values to an array in z3?
It's a bug. Check out this issue.