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

(set-logic QF_ALIA)
(set-info :status unsat)
(declare-const all1 (Array Int Int))
(declare-const a Int)
(declare-const i Int)
(assert (= all1 ((as const (Array Int Int)) 1)))
(assert (= a (select all1 i)))
(assert (not (= a 1)))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback