; EXIT: 1
; EXPECT: (error "Array theory solver does not yet support write-chains connecting two different constant arrays")
(set-logic ALL)
(set-option :incremental false)
(declare-fun all1 () (Array Int Int))
(declare-fun all2 () (Array Int Int))
(declare-fun aa () (Array Int Int))
(declare-fun bb () (Array Int Int))
(declare-fun a () Int)
(declare-fun i () Int)
(assert (= all1 ((as const (Array Int Int)) 1)))
(assert (= aa (store all1 i 0)))
(assert (= all2 ((as const (Array Int Int)) 2)))
(assert (= bb (store all2 i 0)))
(assert (= aa bb))
(check-sat)