(set-info :smt-lib-version 2.6)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with k-induction on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :category "industrial")
(set-info :status unsat)


(define-fun _1 () Bool true)
(declare-fun |main::lk1@3| () Real)
(declare-fun |main::lk1@6| () Real)
(declare-fun |main::lk3@4| () Real)
(declare-fun |main::p3@1| () Real)
(declare-fun |main::lk2@2| () Real)
(declare-fun |main::lk6@4| () Real)
(declare-fun |main::lk1@2| () Real)
(declare-fun |main::lk1@5| () Real)
(declare-fun |main::lk5@2| () Real)
(declare-fun |main::lk5@6| () Real)
(declare-fun |main::cond@2| () Real)
(declare-fun |main::lk4@2| () Real)
(declare-fun |main::lk3@7| () Real)
(declare-fun |main::lk2@5| () Real)
(declare-fun |main::lk1@7| () Real)
(declare-fun |main::lk4@3| () Real)
(declare-fun |main::lk3@5| () Real)
(declare-fun |main::lk4@7| () Real)
(declare-fun |main::lk4@5| () Real)
(declare-fun |main::lk2@4| () Real)
(declare-fun |main::lk5@3| () Real)
(declare-fun |main::lk5@5| () Real)
(declare-fun |main::lk3@3| () Real)
(declare-fun |main::lk3@2| () Real)
(declare-fun |main::lk4@6| () Real)
(declare-fun |main::lk6@3| () Real)
(declare-fun |main::lk6@5| () Real)
(declare-fun |main::lk6@2| () Real)
(declare-fun |main::lk4@4| () Real)
(declare-fun |main::lk2@7| () Real)
(declare-fun |main::lk5@7| () Real)
(declare-fun |main::lk3@6| () Real)
(declare-fun |main::lk6@6| () Real)
(declare-fun |main::cond@3| () Real)
(declare-fun |main::p4@1| () Real)
(declare-fun |main::p1@1| () Real)
(declare-fun |main::lk2@6| () Real)
(declare-fun |main::lk1@4| () Real)
(declare-fun |main::lk2@3| () Real)
(declare-fun |main::p5@1| () Real)
(declare-fun |main::p2@1| () Real)
(declare-fun |main::p6@1| () Real)
(declare-fun |main::lk5@4| () Real)
(define-fun _7 () Real 0)
(define-fun _59 () Real |main::cond@3|)
(define-fun _60 () Bool (= _59 _7))
(define-fun _61 () Real 1)
(define-fun _64 () Bool (not _60))
(define-fun _66 () Real |main::lk1@3|)
(define-fun _69 () Real |main::lk2@3|)
(define-fun _72 () Real |main::lk3@3|)
(define-fun _75 () Real |main::lk4@3|)
(define-fun _78 () Real |main::lk5@3|)
(define-fun _81 () Real |main::lk6@3|)
(define-fun _90 () Real |main::lk1@4|)
(define-fun _93 () Bool (= _66 _90))
(define-fun _102 () Real |main::lk2@4|)
(define-fun _105 () Bool (= _69 _102))
(define-fun _114 () Real |main::lk3@4|)
(define-fun _117 () Bool (= _72 _114))
(define-fun _126 () Real |main::lk4@4|)
(define-fun _129 () Bool (= _75 _126))
(define-fun _138 () Real |main::lk5@4|)
(define-fun _141 () Bool (= _78 _138))
(define-fun _150 () Real |main::lk6@4|)
(define-fun _153 () Bool (= _81 _150))
(define-fun _162 () Real |main::lk1@5|)
(define-fun _163 () Bool (= _162 _7))
(define-fun _174 () Real |main::lk2@5|)
(define-fun _175 () Bool (= _174 _7))
(define-fun _186 () Real |main::lk3@5|)
(define-fun _187 () Bool (= _186 _7))
(define-fun _198 () Real |main::lk4@5|)
(define-fun _199 () Bool (= _198 _7))
(define-fun _210 () Real |main::lk5@5|)
(define-fun _211 () Bool (= _210 _7))
(define-fun _222 () Real |main::lk6@5|)
(define-fun _223 () Bool (= _222 _7))
(define-fun _253 () Real |main::cond@2|)
(define-fun _254 () Bool (= _253 _7))
(define-fun _256 () Bool (not _254))
(define-fun _257 () Real |main::lk1@2|)
(define-fun _258 () Bool (= _257 _7))
(define-fun _259 () Bool (and _256 _258))
(define-fun _260 () Real |main::lk2@2|)
(define-fun _261 () Bool (= _260 _7))
(define-fun _262 () Bool (and _259 _261))
(define-fun _263 () Real |main::lk3@2|)
(define-fun _264 () Bool (= _263 _7))
(define-fun _265 () Bool (and _262 _264))
(define-fun _266 () Real |main::lk4@2|)
(define-fun _267 () Bool (= _266 _7))
(define-fun _268 () Bool (and _265 _267))
(define-fun _269 () Real |main::lk5@2|)
(define-fun _270 () Bool (= _269 _7))
(define-fun _271 () Bool (and _268 _270))
(define-fun _272 () Real |main::lk6@2|)
(define-fun _273 () Bool (= _272 _7))
(define-fun _274 () Bool (and _271 _273))
(define-fun _275 () Real |main::p1@1|)
(define-fun _276 () Bool (= _275 _7))
(define-fun _277 () Bool (not _276))
(define-fun _279 () Bool (and _274 _277))
(define-fun _280 () Bool (and _274 _276))
(define-fun _281 () Bool (= _66 _61))
(define-fun _282 () Bool (and _279 _281))
(define-fun _283 () Bool (= _66 _257))
(define-fun _284 () Bool (and _280 _283))
(define-fun _285 () Bool (or _282 _284))
(define-fun _286 () Real |main::p2@1|)
(define-fun _287 () Bool (= _286 _7))
(define-fun _288 () Bool (not _287))
(define-fun _290 () Bool (and _285 _288))
(define-fun _291 () Bool (and _285 _287))
(define-fun _292 () Bool (= _69 _61))
(define-fun _293 () Bool (and _290 _292))
(define-fun _294 () Bool (= _69 _260))
(define-fun _295 () Bool (and _291 _294))
(define-fun _296 () Bool (or _293 _295))
(define-fun _297 () Real |main::p3@1|)
(define-fun _298 () Bool (= _297 _7))
(define-fun _299 () Bool (not _298))
(define-fun _301 () Bool (and _296 _299))
(define-fun _302 () Bool (and _296 _298))
(define-fun _303 () Bool (= _72 _61))
(define-fun _304 () Bool (and _301 _303))
(define-fun _305 () Bool (= _72 _263))
(define-fun _306 () Bool (and _302 _305))
(define-fun _307 () Bool (or _304 _306))
(define-fun _308 () Real |main::p4@1|)
(define-fun _309 () Bool (= _308 _7))
(define-fun _310 () Bool (not _309))
(define-fun _312 () Bool (and _307 _310))
(define-fun _313 () Bool (and _307 _309))
(define-fun _314 () Bool (= _75 _61))
(define-fun _315 () Bool (and _312 _314))
(define-fun _316 () Bool (= _75 _266))
(define-fun _317 () Bool (and _313 _316))
(define-fun _318 () Bool (or _315 _317))
(define-fun _319 () Real |main::p5@1|)
(define-fun _320 () Bool (= _319 _7))
(define-fun _321 () Bool (not _320))
(define-fun _323 () Bool (and _318 _321))
(define-fun _324 () Bool (and _318 _320))
(define-fun _325 () Bool (= _78 _61))
(define-fun _326 () Bool (and _323 _325))
(define-fun _327 () Bool (= _78 _269))
(define-fun _328 () Bool (and _324 _327))
(define-fun _329 () Bool (or _326 _328))
(define-fun _330 () Real |main::p6@1|)
(define-fun _331 () Bool (= _330 _7))
(define-fun _332 () Bool (not _331))
(define-fun _334 () Bool (and _329 _332))
(define-fun _335 () Bool (and _329 _331))
(define-fun _336 () Bool (= _81 _61))
(define-fun _337 () Bool (and _334 _336))
(define-fun _338 () Bool (= _81 _272))
(define-fun _339 () Bool (and _335 _338))
(define-fun _340 () Bool (or _337 _339))
(define-fun _341 () Bool (and _277 _340))
(define-fun _342 () Bool (and _276 _340))
(define-fun _346 () Bool (and _281 _341))
(define-fun _347 () Bool (= _90 _7))
(define-fun _348 () Bool (and _346 _347))
(define-fun _349 () Bool (and _93 _342))
(define-fun _350 () Bool (or _348 _349))
(define-fun _351 () Bool (and _288 _350))
(define-fun _352 () Bool (and _287 _350))
(define-fun _356 () Bool (and _292 _351))
(define-fun _357 () Bool (= _102 _7))
(define-fun _358 () Bool (and _356 _357))
(define-fun _359 () Bool (and _105 _352))
(define-fun _360 () Bool (or _358 _359))
(define-fun _361 () Bool (and _299 _360))
(define-fun _362 () Bool (and _298 _360))
(define-fun _366 () Bool (and _303 _361))
(define-fun _367 () Bool (= _114 _7))
(define-fun _368 () Bool (and _366 _367))
(define-fun _369 () Bool (and _117 _362))
(define-fun _370 () Bool (or _368 _369))
(define-fun _371 () Bool (and _310 _370))
(define-fun _372 () Bool (and _309 _370))
(define-fun _376 () Bool (and _314 _371))
(define-fun _377 () Bool (= _126 _7))
(define-fun _378 () Bool (and _376 _377))
(define-fun _379 () Bool (and _129 _372))
(define-fun _380 () Bool (or _378 _379))
(define-fun _381 () Bool (and _321 _380))
(define-fun _382 () Bool (and _320 _380))
(define-fun _386 () Bool (and _325 _381))
(define-fun _387 () Bool (= _138 _7))
(define-fun _388 () Bool (and _386 _387))
(define-fun _389 () Bool (and _141 _382))
(define-fun _390 () Bool (or _388 _389))
(define-fun _391 () Bool (and _332 _390))
(define-fun _392 () Bool (and _331 _390))
(define-fun _396 () Bool (and _336 _391))
(define-fun _397 () Bool (= _150 _7))
(define-fun _398 () Bool (and _396 _397))
(define-fun _399 () Bool (and _153 _392))
(define-fun _400 () Bool (or _398 _399))
(define-fun _402 () Bool (and _64 _400))
(define-fun _424 () Bool (and _163 _402))
(define-fun _425 () Bool (and _175 _424))
(define-fun _426 () Bool (and _187 _425))
(define-fun _427 () Bool (and _199 _426))
(define-fun _428 () Bool (and _211 _427))
(define-fun _429 () Bool (and _223 _428))
(define-fun _430 () Bool (and _277 _429))
(define-fun _431 () Bool (and _276 _429))
(define-fun _432 () Real |main::lk1@6|)
(define-fun _433 () Bool (= _432 _61))
(define-fun _434 () Bool (and _430 _433))
(define-fun _435 () Bool (= _162 _432))
(define-fun _436 () Bool (and _431 _435))
(define-fun _437 () Bool (or _434 _436))
(define-fun _438 () Bool (and _288 _437))
(define-fun _439 () Bool (and _287 _437))
(define-fun _440 () Real |main::lk2@6|)
(define-fun _441 () Bool (= _440 _61))
(define-fun _442 () Bool (and _438 _441))
(define-fun _443 () Bool (= _174 _440))
(define-fun _444 () Bool (and _439 _443))
(define-fun _445 () Bool (or _442 _444))
(define-fun _446 () Bool (and _299 _445))
(define-fun _447 () Bool (and _298 _445))
(define-fun _448 () Real |main::lk3@6|)
(define-fun _449 () Bool (= _448 _61))
(define-fun _450 () Bool (and _446 _449))
(define-fun _451 () Bool (= _186 _448))
(define-fun _452 () Bool (and _447 _451))
(define-fun _453 () Bool (or _450 _452))
(define-fun _454 () Bool (and _310 _453))
(define-fun _455 () Bool (and _309 _453))
(define-fun _456 () Real |main::lk4@6|)
(define-fun _457 () Bool (= _456 _61))
(define-fun _458 () Bool (and _454 _457))
(define-fun _459 () Bool (= _198 _456))
(define-fun _460 () Bool (and _455 _459))
(define-fun _461 () Bool (or _458 _460))
(define-fun _462 () Bool (and _321 _461))
(define-fun _463 () Bool (and _320 _461))
(define-fun _464 () Real |main::lk5@6|)
(define-fun _465 () Bool (= _464 _61))
(define-fun _466 () Bool (and _462 _465))
(define-fun _467 () Bool (= _210 _464))
(define-fun _468 () Bool (and _463 _467))
(define-fun _469 () Bool (or _466 _468))
(define-fun _470 () Bool (and _332 _469))
(define-fun _471 () Bool (and _331 _469))
(define-fun _472 () Real |main::lk6@6|)
(define-fun _473 () Bool (= _472 _61))
(define-fun _474 () Bool (and _470 _473))
(define-fun _475 () Bool (= _222 _472))
(define-fun _476 () Bool (and _471 _475))
(define-fun _477 () Bool (or _474 _476))
(define-fun _478 () Bool (and _277 _477))
(define-fun _479 () Bool (and _276 _477))
(define-fun _483 () Bool (and _433 _478))
(define-fun _498 () Real |main::lk1@7|)
(define-fun _499 () Bool (= _498 _7))
(define-fun _500 () Bool (and _483 _499))
(define-fun _501 () Bool (= _432 _498))
(define-fun _502 () Bool (and _479 _501))
(define-fun _503 () Bool (or _500 _502))
(define-fun _504 () Bool (and _288 _503))
(define-fun _505 () Bool (and _287 _503))
(define-fun _509 () Bool (and _441 _504))
(define-fun _519 () Real |main::lk2@7|)
(define-fun _520 () Bool (= _519 _7))
(define-fun _521 () Bool (and _509 _520))
(define-fun _522 () Bool (= _440 _519))
(define-fun _523 () Bool (and _505 _522))
(define-fun _524 () Bool (or _521 _523))
(define-fun _525 () Bool (and _299 _524))
(define-fun _526 () Bool (and _298 _524))
(define-fun _530 () Bool (and _449 _525))
(define-fun _539 () Real |main::lk3@7|)
(define-fun _540 () Bool (= _539 _7))
(define-fun _541 () Bool (and _530 _540))
(define-fun _542 () Bool (= _448 _539))
(define-fun _543 () Bool (and _526 _542))
(define-fun _544 () Bool (or _541 _543))
(define-fun _545 () Bool (and _310 _544))
(define-fun _546 () Bool (and _309 _544))
(define-fun _550 () Bool (and _457 _545))
(define-fun _558 () Real |main::lk4@7|)
(define-fun _559 () Bool (= _558 _7))
(define-fun _560 () Bool (and _550 _559))
(define-fun _561 () Bool (= _456 _558))
(define-fun _562 () Bool (and _546 _561))
(define-fun _563 () Bool (or _560 _562))
(define-fun _564 () Bool (and _321 _563))
(define-fun _565 () Bool (and _320 _563))
(define-fun _569 () Bool (and _465 _564))
(define-fun _576 () Real |main::lk5@7|)
(define-fun _577 () Bool (= _576 _7))
(define-fun _578 () Bool (and _569 _577))
(define-fun _579 () Bool (= _464 _576))
(define-fun _580 () Bool (and _565 _579))
(define-fun _581 () Bool (or _578 _580))
(define-fun _582 () Bool (and _332 _581))
(define-fun _622 () Bool (not _545))
(define-fun _623 () Bool (or _457 _622))
(define-fun _625 () Bool (not _478))
(define-fun _626 () Bool (or _433 _625))
(define-fun _627 () Bool (and _623 _626))
(define-fun _629 () Bool (not _582))
(define-fun _630 () Bool (or _473 _629))
(define-fun _631 () Bool (and _627 _630))
(define-fun _633 () Bool (not _504))
(define-fun _634 () Bool (or _441 _633))
(define-fun _635 () Bool (and _631 _634))
(define-fun _637 () Bool (not _564))
(define-fun _638 () Bool (or _465 _637))
(define-fun _639 () Bool (and _635 _638))
(define-fun _641 () Bool (not _525))
(define-fun _642 () Bool (or _449 _641))
(define-fun _643 () Bool (and _639 _642))
(define-fun _644 () Bool (not _643))



(assert _1)

(assert _644)
(check-sat)


(exit)
