blob: d514fff70338ea5fc1fb10b3c883b15e51c00938 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
; EXIT: 1
; EXPECT: (error "Array theory solver does not yet support write-chains connecting two different constant arrays")
(set-logic QF_ALIA)
(set-info :status unsat)
(declare-const all1 (Array Int Int))
(declare-const all2 (Array Int Int))
(declare-const aa (Array Int Int))
(declare-const bb (Array Int Int))
(declare-const a Int)
(declare-const 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)
|
