; COMMAND-LINE: --incremental
; EXPECT: sat
; EXPECT: unsat

(set-logic QF_UFLIA)
(declare-fun _base () Int)
(declare-fun _n () Int)
(assert (let ((.def_5 (<= 0 _n)))
.def_5
))
(declare-fun ___z3z___ (Int) Bool)
(declare-fun ___z4z___ (Int) Bool)
(declare-fun ___z5z___ (Int) Bool)
(declare-fun ___z6z___ (Int) Bool)
(push 1)
(assert (let ((.def_120 (= _base 0)))
(let ((.def_119 (___z6z___ (- 1))))
(let ((.def_121 (or .def_119 .def_120)))
(let ((.def_99 (___z4z___ 0)))
(let ((.def_122 (= .def_99 .def_121)))
.def_122
))))))
(assert (let ((.def_190 (+ _n (- 1))))
(let ((.def_222 (+ (- 1) .def_190)))
(let ((.def_234 (___z5z___ .def_222)))
(let ((.def_224 (* (- 1) _base)))
(let ((.def_225 (+ _n .def_224)))
(let ((.def_226 (= .def_225 1)))
(let ((.def_235 (or .def_226 .def_234)))
(let ((.def_229 (not .def_226)))
(let ((.def_236 (and .def_229 .def_235)))
(let ((.def_191 (___z6z___ .def_190)))
(let ((.def_237 (= .def_191 .def_236)))
.def_237
))))))))))))
(check-sat)
(pop 1)
(assert (let ((.def_188 (___z3z___ _n)))
(let ((.def_170 (___z4z___ _n)))
(let ((.def_179 (not .def_170)))
(let ((.def_169 (___z5z___ _n)))
(let ((.def_175 (not .def_169)))
(let ((.def_182 (or .def_175 .def_179)))
(let ((.def_172 (___z6z___ _n)))
(let ((.def_183 (or .def_172 .def_182)))
(let ((.def_180 (and .def_169 .def_179)))
(let ((.def_177 (not .def_172)))
(let ((.def_181 (and .def_177 .def_180)))
(let ((.def_184 (or .def_181 .def_183)))
(let ((.def_176 (and .def_170 .def_175)))
(let ((.def_178 (and .def_176 .def_177)))
(let ((.def_185 (or .def_178 .def_184)))
(let ((.def_171 (and .def_169 .def_170)))
(let ((.def_173 (and .def_171 .def_172)))
(let ((.def_186 (or .def_173 .def_185)))
(let ((.def_174 (not .def_173)))
(let ((.def_187 (and .def_174 .def_186)))
(let ((.def_189 (= .def_187 .def_188)))
.def_189
))))))))))))))))))))))
(assert (let ((.def_192 (= _n _base)))
(let ((.def_190 (+ _n (- 1))))
(let ((.def_191 (___z6z___ .def_190)))
(let ((.def_193 (or .def_191 .def_192)))
(let ((.def_170 (___z4z___ _n)))
(let ((.def_194 (= .def_170 .def_193)))
.def_194
)))))))
(assert (let ((.def_190 (+ _n (- 1))))
(let ((.def_196 (___z4z___ .def_190)))
(let ((.def_192 (= _n _base)))
(let ((.def_197 (or .def_192 .def_196)))
(let ((.def_195 (not .def_192)))
(let ((.def_198 (and .def_195 .def_197)))
(let ((.def_169 (___z5z___ _n)))
(let ((.def_199 (= .def_169 .def_198)))
.def_199
)))))))))
(assert (let ((.def_313 (+ _n (- 3))))
(let ((.def_314 (___z3z___ .def_313)))
.def_314
)))
(assert (let ((.def_224 (* (- 1) _base)))
(let ((.def_225 (+ _n .def_224)))
(let ((.def_226 (= .def_225 1)))
(let ((.def_190 (+ _n (- 1))))
(let ((.def_222 (+ (- 1) .def_190)))
(let ((.def_223 (___z6z___ .def_222)))
(let ((.def_227 (or .def_223 .def_226)))
(let ((.def_196 (___z4z___ .def_190)))
(let ((.def_228 (= .def_196 .def_227)))
.def_228
))))))))))
(assert (let ((.def_190 (+ _n (- 1))))
(let ((.def_222 (+ (- 1) .def_190)))
(let ((.def_234 (___z5z___ .def_222)))
(let ((.def_224 (* (- 1) _base)))
(let ((.def_225 (+ _n .def_224)))
(let ((.def_226 (= .def_225 1)))
(let ((.def_235 (or .def_226 .def_234)))
(let ((.def_229 (not .def_226)))
(let ((.def_236 (and .def_229 .def_235)))
(let ((.def_191 (___z6z___ .def_190)))
(let ((.def_237 (= .def_191 .def_236)))
.def_237
))))))))))))
(push 1)
(assert (let ((.def_240 (+ _n (- 2))))
(let ((.def_297 (+ (- 1) .def_240)))
(let ((.def_303 (___z4z___ .def_297)))
(let ((.def_224 (* (- 1) _base)))
(let ((.def_225 (+ _n .def_224)))
(let ((.def_299 (= .def_225 2)))
(let ((.def_304 (or .def_299 .def_303)))
(let ((.def_302 (not .def_299)))
(let ((.def_305 (and .def_302 .def_304)))
(let ((.def_277 (___z5z___ .def_240)))
(let ((.def_306 (= .def_277 .def_305)))
.def_306
))))))))))))
(assert (let ((.def_240 (+ _n (- 2))))
(let ((.def_297 (+ (- 1) .def_240)))
(let ((.def_307 (___z5z___ .def_297)))
(let ((.def_224 (* (- 1) _base)))
(let ((.def_225 (+ _n .def_224)))
(let ((.def_299 (= .def_225 2)))
(let ((.def_308 (or .def_299 .def_307)))
(let ((.def_302 (not .def_299)))
(let ((.def_309 (and .def_302 .def_308)))
(let ((.def_280 (___z6z___ .def_240)))
(let ((.def_310 (= .def_280 .def_309)))
.def_310
))))))))))))
(assert (let ((.def_313 (+ _n (- 3))))
(let ((.def_351 (___z4z___ .def_313)))
(let ((.def_360 (not .def_351)))
(let ((.def_350 (___z5z___ .def_313)))
(let ((.def_356 (not .def_350)))
(let ((.def_363 (or .def_356 .def_360)))
(let ((.def_353 (___z6z___ .def_313)))
(let ((.def_364 (or .def_353 .def_363)))
(let ((.def_361 (and .def_350 .def_360)))
(let ((.def_358 (not .def_353)))
(let ((.def_362 (and .def_358 .def_361)))
(let ((.def_365 (or .def_362 .def_364)))
(let ((.def_357 (and .def_351 .def_356)))
(let ((.def_359 (and .def_357 .def_358)))
(let ((.def_366 (or .def_359 .def_365)))
(let ((.def_352 (and .def_350 .def_351)))
(let ((.def_354 (and .def_352 .def_353)))
(let ((.def_367 (or .def_354 .def_366)))
(let ((.def_355 (not .def_354)))
(let ((.def_368 (and .def_355 .def_367)))
(let ((.def_314 (___z3z___ .def_313)))
(let ((.def_369 (= .def_314 .def_368)))
.def_369
)))))))))))))))))))))))
(assert (let ((.def_334 (= _base (- 3))))
(let ((.def_337 (not .def_334)))
(let ((.def_188 (___z3z___ _n)))
(let ((.def_384 (or .def_188 .def_337)))
(let ((.def_385 (not .def_384)))
.def_385
))))))
(check-sat)