blob: 30a6876082276c3fc72cd83f166706a2c544cf3c (
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 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)
|
