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

(set-logic QF_ALIA)
(set-info :status unsat)
(declare-const all1 (Array Int Int))
(declare-const all2 (Array Int Int))
(declare-const a Int)
(declare-const 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