1; COMMAND-LINE: --incremental
2; EXPECT: sat
3; EXPECT: sat
4; EXPECT: unsat
5; EXIT: 0
6(set-logic QF_BVFS)
7(declare-fun S1 () (Set (_ BitVec 1)))
8(declare-fun S2 () (Set (_ BitVec 1)))
9(declare-fun S3 () (Set (_ BitVec 1)))
10(declare-fun S4 () (Set (_ BitVec 1)))
11(assert (distinct S1 S2 S3 S4))
12(check-sat)
13;(get-model)
14(declare-fun S5 () (Set (_ BitVec 1)))
15(assert (not (= S5 S1)))
16(assert (not (= S5 S2)))
17(assert (not (= S5 S3)))
18(check-sat)
19(assert (not (= S5 S4)))
20(check-sat)
21