summaryrefslogtreecommitdiff
path: root/test/regress/regress0/boolean-terms-bug-array.smt2
blob: 1183487f90c2ff9b878c6ef992dae8dcf21f93f6 (plain) 
1
2
3
4
5
6
7
8
9

(set-logic AUFLIRA)
(set-info :status sat)

(declare-fun f ((Array Int Bool)) Bool)
(declare-fun y () (Array Int Bool))

(assert (forall ((x (Array Int Bool))) (f y)))

(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback