blob: 1c28759b606921ba74b7b1a9f93dd49b234d87e6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
(set-logic QF_ALL)
(set-info :status unsat)
; Observed
;
; sat as output instead of unsat
;
; What was going on?
;
; The solver was unable to reason that (emptyset) cannot equal
; (singleton 0). There were no membership predicates anywhere, just
; equalities.
;
; Fix
;
; Add the propagation rule: (true) => (member x (singleton x))
(declare-fun z3f70 (Int) (Set Int))
(declare-fun z3v85 () Int)
(declare-fun z3v86 () Int)
(declare-fun z3v87 () Int)
(declare-fun z3v90 () Int)
(assert (= (z3f70 z3v90) (union (z3f70 z3v85) (union (as emptyset (Set Int)) (singleton z3v86)))))
(assert (= (z3f70 z3v90) (z3f70 z3v87)))
(assert (= (as emptyset (Set Int)) (z3f70 z3v87)))
(check-sat)
|
