summaryrefslogtreecommitdiff
path: root/test/regress/regress1/bags/choose4.smt2
blob: a0290b90b57b527799d20ab404c0c35bb4f6b7f0 (plain) 
1
2
3
4
5
6
7
8
9

; COMMAND-LINE: --quiet
(set-logic ALL)
(set-info :status sat)
(declare-fun A () (Bag Int))
(declare-fun a () Int)
(assert (not (= A (as emptybag (Bag Int)))))
(assert (> (bag.count 10 A) 0))
(assert (= a (bag.choose A)))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback