(set-logic ALL) (set-info :status unsat) (declare-fun A () (Bag String)) (declare-fun x () String) (declare-fun y () Int) (assert (= x "x")) (assert (= A (as emptybag (Bag String)))) (assert (= (bag.count x A) y)) (assert(> y 1)) (check-sat)