1; COMMAND-LINE: --incremental 2; EXPECT: unsat 3; EXPECT: sat 4 5; x not in A U B => x not in A 6(set-logic ALL_SUPPORTED) 7(define-sort SetInt () (Set Int)) 8(declare-fun A () (Set Int)) 9(declare-fun B () (Set Int)) 10(declare-fun x () Int) 11(assert (member x A)) 12(push 1) 13(assert (not (member x (union A B)))) 14(check-sat) 15(pop 1) 16(check-sat) 17