1 2 3 4 5 6 7 8 9 10
(set-logic ALL) (set-info :status sat) (set-option :produce-models true) (declare-fun A () (Bag String)) (declare-fun B () (Bag String)) (declare-fun C () (Bag String)) (assert (= C (intersection_min A B))) (assert (distinct (as emptybag (Bag String)) C)) (assert (distinct A B C)) (check-sat)