(set-logic ALL) (set-info :status sat) (declare-fun A () (Bag Int)) (declare-fun B () (Bag Int)) (declare-fun x () Int) (declare-fun y () Int) (assert (= A (union_max (bag x 1) (bag y 2)))) (assert (= A (union_disjoint B (bag y 2)))) (assert (= x y)) (check-sat)