1 2 3 4 5 6 7 8
(set-logic ALL) (set-info :status unsat) (declare-fun A () (Bag String)) (declare-fun B () (Bag String)) (assert (= B (bag.duplicate_removal A))) (assert (distinct (as bag.empty (Bag String)) A B)) (assert (= B (bag.union_max A B))) (check-sat)