summaryrefslogtreecommitdiff
path: root/test/regress/regress0/arrays/constarr2.cvc.smt2
blob: 52704cea76664b38012e43795d5495d18b183df7 (plain) 
1
2
3
4
5
6
7
8
9
10
11

; EXPECT: unsat
(set-logic ALL)
(set-option :incremental false)
(declare-fun all1 () (Array Int Int))
(declare-fun all2 () (Array Int Int))
(declare-fun a () Int)
(declare-fun i () Int)
(assert (= all1 ((as const (Array Int Int)) 1)))
(assert (= all2 ((as const (Array Int Int)) 2)))
(assert (= all1 all2))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback