1; COMMAND-LINE: --lang=smt2.5 --incremental
2; EXPECT: sat
3; EXPECT: sat
4(set-logic ALL)
5
6(declare-datatypes () ((Unit (uu))))
7
8(declare-fun y () Int)
9(declare-fun b () Bool)
10(declare-fun s () (Set Int))
11(declare-fun u () Unit)
12
13(assert (= s (insert y s)))
14(assert (=> b (= uu u)))
15
16(push 1)
17(check-sat)
18(pop 1)
19
20(push 1)
21(check-sat)
22