path: root/test/regress/regress0/sets/fuzz15201.smt2

; symptom: unsat instead of sat
; issue/fix: buggy rewriter for setminus
(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status sat)
(set-logic QF_UFLIAFS)
(define-sort Element () Int)
(declare-fun f0 ( Int) Int)
(declare-fun f1 ( (Set Element)) (Set Element))
(declare-fun p0 ( Int) Bool)
(declare-fun p1 ( (Set Element) (Set Element) (Set Element)) Bool)
(declare-fun v0 () Int)
(declare-fun v1 () (Set Element))
(declare-fun v2 () (Set Element))
(assert (let ((e3 0))
(let ((e4 (+ v0 v0)))
(let ((e5 (+ v0 e4)))
(let ((e6 (* (- e3) e4)))
(let ((e7 (- e4 e6)))
(let ((e8 (+ e7 e5)))
(let ((e9 (- v0)))
(let ((e10 (* e6 e3)))
(let ((e11 (- e8 e5)))
(let ((e12 (- e5)))
(let ((e13 (* e7 (- e3))))
(let ((e14 (f0 e7)))
(let ((e15 (ite (p0 e9) 1 0)))
(let ((e16 (setminus v2 v1)))
(let ((e17 (setminus v1 v2)))
(let ((e18 (union e17 e17)))
(let ((e19 (intersection e17 v1)))
(let ((e20 (intersection e17 e18)))
(let ((e21 (intersection v1 e16)))
(let ((e22 (setminus e20 e16)))
(let ((e23 (ite (p1 v2 e18 e21) (singleton 1) (singleton 0))))
(let ((e24 (setminus e17 e23)))
(let ((e25 (union v2 e22)))
(let ((e26 (union e24 e18)))
(let ((e27 (ite (p1 e20 e19 e25) (singleton 1) (singleton 0))))
(let ((e28 (f1 e20)))
(let ((e29 (member e14 e17)))
(let ((e30 (member e13 e23)))
(let ((e31 (member e11 e25)))
(let ((e32 (member e6 v1)))
(let ((e33 (member e9 v1)))
(let ((e34 (member v0 e28)))
(let ((e35 (member e9 e16)))
(let ((e36 (member e4 e17)))
(let ((e37 (member e9 e18)))
(let ((e38 (member e14 e25)))
(let ((e39 (member e14 v2)))
(let ((e40 (member v0 v1)))
(let ((e41 (member e4 e16)))
(let ((e42 (member e15 e21)))
(let ((e43 (member e7 e22)))
(let ((e44 (member e11 v2)))
(let ((e45 (member e14 e22)))
(let ((e46 (member e11 e16)))
(let ((e47 (member e15 e22)))
(let ((e48 (member e10 e23)))
(let ((e49 (member e4 e21)))
(let ((e50 (member e5 e28)))
(let ((e51 (member e6 e28)))
(let ((e52 (member v0 e22)))
(let ((e53 (member e14 e20)))
(let ((e54 (f1 e21)))
(let ((e55 (f1 e28)))
(let ((e56 (f1 e27)))
(let ((e57 (f1 e17)))
(let ((e58 (f1 e22)))
(let ((e59 (f1 e26)))
(let ((e60 (f1 e19)))
(let ((e61 (f1 v1)))
(let ((e62 (f1 e24)))
(let ((e63 (f1 e20)))
(let ((e64 (f1 e23)))
(let ((e65 (f1 v2)))
(let ((e66 (f1 e25)))
(let ((e67 (f1 e62)))
(let ((e68 (f1 e18)))
(let ((e69 (f1 e18)))
(let ((e70 (f1 e23)))
(let ((e71 (f1 e55)))
(let ((e72 (f1 e26)))
(let ((e73 (f1 e16)))
(let ((e74 (= e13 e13)))
(let ((e75 (p0 e11)))
(let ((e76 (distinct e15 e4)))
(let ((e77 (> e14 e10)))
(let ((e78 (= e4 e15)))
(let ((e79 (distinct v0 e9)))
(let ((e80 (= e15 e14)))
(let ((e81 (>= e10 e11)))
(let ((e82 (distinct e9 e8)))
(let ((e83 (p0 v0)))
(let ((e84 (>= e12 e14)))
(let ((e85 (distinct e7 e13)))
(let ((e86 (<= e6 e11)))
(let ((e87 (= e13 e10)))
(let ((e88 (>= e7 e8)))
(let ((e89 (<= v0 e10)))
(let ((e90 (>= e5 e15)))
(let ((e91 (ite e33 e66 e26)))
(let ((e92 (ite e88 e54 v1)))
(let ((e93 (ite e76 e70 e16)))
(let ((e94 (ite e85 e19 e24)))
(let ((e95 (ite e88 e68 e20)))
(let ((e96 (ite e86 e25 e65)))
(let ((e97 (ite e83 v2 e23)))
(let ((e98 (ite e50 e63 e63)))
(let ((e99 (ite e48 e56 e93)))
(let ((e100 (ite e38 e60 v2)))
(let ((e101 (ite e30 e61 e61)))
(let ((e102 (ite e85 e69 e57)))
(let ((e103 (ite e83 e18 e102)))
(let ((e104 (ite e43 e62 e97)))
(let ((e105 (ite e76 e27 e21)))
(let ((e106 (ite e89 e92 e55)))
(let ((e107 (ite e46 e72 e65)))
(let ((e108 (ite e79 e71 e97)))
(let ((e109 (ite e44 e64 e21)))
(let ((e110 (ite e33 e70 e25)))
(let ((e111 (ite e43 e63 e105)))
(let ((e112 (ite e39 e56 e108)))
(let ((e113 (ite e49 e17 e107)))
(let ((e114 (ite e74 e63 e113)))
(let ((e115 (ite e84 e28 v1)))
(let ((e116 (ite e82 e68 e67)))
(let ((e117 (ite e75 e73 e21)))
(let ((e118 (ite e36 e59 e16)))
(let ((e119 (ite e48 e118 e61)))
(let ((e120 (ite e90 e56 e100)))
(let ((e121 (ite e80 e24 e25)))
(let ((e122 (ite e31 e22 v2)))
(let ((e123 (ite e45 e107 e16)))
(let ((e124 (ite e40 e70 e73)))
(let ((e125 (ite e52 e58 e118)))
(let ((e126 (ite e88 e72 e72)))
(let ((e127 (ite e35 e58 e27)))
(let ((e128 (ite e42 e59 e21)))
(let ((e129 (ite e44 e127 e103)))
(let ((e130 (ite e51 e118 e69)))
(let ((e131 (ite e37 e16 e24)))
(let ((e132 (ite e83 e105 e28)))
(let ((e133 (ite e48 e107 e60)))
(let ((e134 (ite e34 e101 e22)))
(let ((e135 (ite e86 e97 e57)))
(let ((e136 (ite e47 e94 e100)))
(let ((e137 (ite e78 e104 e95)))
(let ((e138 (ite e75 e26 e96)))
(let ((e139 (ite e35 e97 e121)))
(let ((e140 (ite e44 e112 e118)))
(let ((e141 (ite e77 e107 e56)))
(let ((e142 (ite e53 e64 e129)))
(let ((e143 (ite e48 e128 e23)))
(let ((e144 (ite e50 e73 e17)))
(let ((e145 (ite e33 e98 e114)))
(let ((e146 (ite e32 e137 e105)))
(let ((e147 (ite e41 e98 e96)))
(let ((e148 (ite e29 e93 e121)))
(let ((e149 (ite e87 e104 e21)))
(let ((e150 (ite e46 e131 e110)))
(let ((e151 (ite e81 e25 e65)))
(let ((e152 (ite e34 e10 e10)))
(let ((e153 (ite e36 e7 e13)))
(let ((e154 (ite e43 e12 e10)))
(let ((e155 (ite e50 e14 e7)))
(let ((e156 (ite e34 e9 e6)))
(let ((e157 (ite e33 e7 v0)))
(let ((e158 (ite e50 e157 e10)))
(let ((e159 (ite e51 e8 e11)))
(let ((e160 (ite e32 v0 e157)))
(let ((e161 (ite e85 e15 e158)))
(let ((e162 (ite e43 e5 e11)))
(let ((e163 (ite e76 e4 v0)))
(let ((e164 (ite e53 e10 e159)))
(let ((e165 (ite e80 e161 e163)))
(let ((e166 (ite e78 e13 e11)))
(let ((e167 (ite e49 e4 e8)))
(let ((e168 (ite e45 e11 e155)))
(let ((e169 (ite e81 e155 e166)))
(let ((e170 (ite e87 e169 e161)))
(let ((e171 (ite e53 e165 e13)))
(let ((e172 (ite e83 e12 e160)))
(let ((e173 (ite e80 e168 e159)))
(let ((e174 (ite e46 e171 e168)))
(let ((e175 (ite e74 e5 e155)))
(let ((e176 (ite e89 e159 e4)))
(let ((e177 (ite e29 e159 e172)))
(let ((e178 (ite e79 e165 e162)))
(let ((e179 (ite e88 e166 e168)))
(let ((e180 (ite e77 e175 e167)))
(let ((e181 (ite e47 e157 e165)))
(let ((e182 (ite e84 e172 e7)))
(let ((e183 (ite e30 e174 e157)))
(let ((e184 (ite e90 e4 e14)))
(let ((e185 (ite e38 e178 e14)))
(let ((e186 (ite e44 e166 e154)))
(let ((e187 (ite e42 e162 e186)))
(let ((e188 (ite e86 e187 e10)))
(let ((e189 (ite e29 e171 e182)))
(let ((e190 (ite e77 e185 e165)))
(let ((e191 (ite e75 e171 e9)))
(let ((e192 (ite e39 e161 e181)))
(let ((e193 (ite e82 e166 e10)))
(let ((e194 (ite e31 e183 e179)))
(let ((e195 (ite e44 e191 e169)))
(let ((e196 (ite e35 e171 e156)))
(let ((e197 (ite e86 e179 e164)))
(let ((e198 (ite e41 e5 e5)))
(let ((e199 (ite e85 e160 e161)))
(let ((e200 (ite e52 e173 e157)))
(let ((e201 (ite e47 e161 e4)))
(let ((e202 (ite e52 e6 e186)))
(let ((e203 (ite e45 e162 e198)))
(let ((e204 (ite e48 e194 e11)))
(let ((e205 (ite e37 e197 e157)))
(let ((e206 (ite e35 e153 e176)))
(let ((e207 (ite e40 e185 e188)))
(let ((e208 (= e53 e41)))
(let ((e209 (not e79)))
(let ((e210 (= e30 e87)))
(let ((e211 (or e34 e48)))
(let ((e212 (=> e82 e29)))
(let ((e213 (xor e77 e211)))
(let ((e214 (and e31 e78)))
(let ((e215 (ite e36 e76 e37)))
(let ((e216 (= e84 e45)))
(let ((e217 (or e43 e46)))
(let ((e218 (and e88 e40)))
(let ((e219 (not e89)))
(let ((e220 (not e35)))
(let ((e221 (or e218 e213)))
(let ((e222 (xor e216 e75)))
(let ((e223 (ite e85 e90 e219)))
(let ((e224 (= e32 e217)))
(let ((e225 (not e39)))
(let ((e226 (xor e212 e49)))
(let ((e227 (and e222 e81)))
(let ((e228 (or e33 e210)))
(let ((e229 (xor e225 e226)))
(let ((e230 (xor e74 e47)))
(let ((e231 (= e220 e38)))
(let ((e232 (xor e231 e229)))
(let ((e233 (and e50 e221)))
(let ((e234 (and e42 e224)))
(let ((e235 (xor e223 e214)))
(let ((e236 (= e234 e228)))
(let ((e237 (and e227 e235)))
(let ((e238 (not e51)))
(let ((e239 (= e80 e232)))
(let ((e240 (or e230 e86)))
(let ((e241 (not e238)))
(let ((e242 (xor e44 e237)))
(let ((e243 (= e236 e242)))
(let ((e244 (= e209 e240)))
(let ((e245 (and e239 e83)))
(let ((e246 (or e208 e245)))
(let ((e247 (=> e215 e246)))
(let ((e248 (ite e233 e247 e244)))
(let ((e249 (and e248 e241)))
(let ((e250 (=> e243 e249)))
(let ((e251 (and e52 e250)))
e251
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
;(get-model)