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