; COMMAND-LINE: --incremental
; EXPECT: sat
; EXPECT: sat
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")


(declare-fun |__ADDRESS_OF_main::c1| () Real)
(declare-fun |__ADDRESS_OF_main::x1| () Real)
(declare-fun |__ADDRESS_OF_main::x2| () Real)
(declare-fun |__ADDRESS_OF_main::c2| () Real)
(declare-fun |main::x3@3| () Real)
(declare-fun |main::x1@3| () Real)
(declare-fun |__ADDRESS_OF_main::d3| () Real)
(declare-fun __BASE_ADDRESS_OF__ (Real) Real)
(declare-fun |main::x2@3| () Real)
(declare-fun |main::d3@2| () Real)
(declare-fun |__VERIFIER_assert::cond@2| () Real)
(declare-fun |__ADDRESS_OF_main::x3| () Real)
(declare-fun |main::d1@2| () Real)
(declare-fun |__ADDRESS_OF_main::d2| () Real)
(declare-fun |__ADDRESS_OF_main::__CPAchecker_TMP_0| () Real)
(declare-fun |main::__CPAchecker_TMP_0@3| () Real)
(declare-fun |__ADDRESS_OF_main::d1| () Real)
(declare-fun |main::d2@2| () Real)
(define-fun _7 () Real 0)
(define-fun _8 () Real |__ADDRESS_OF_main::x1|)
(define-fun _9 () Real (__BASE_ADDRESS_OF__ _8))
(define-fun _10 () Bool (= _8 _9))
(define-fun _11 () Real |__ADDRESS_OF_main::x2|)
(define-fun _12 () Real (__BASE_ADDRESS_OF__ _11))
(define-fun _13 () Bool (= _11 _12))
(define-fun _14 () Bool (and _10 _13))
(define-fun _15 () Real |__ADDRESS_OF_main::x3|)
(define-fun _16 () Real (__BASE_ADDRESS_OF__ _15))
(define-fun _17 () Bool (= _15 _16))
(define-fun _18 () Bool (and _14 _17))
(define-fun _19 () Real |__ADDRESS_OF_main::d1|)
(define-fun _20 () Real (__BASE_ADDRESS_OF__ _19))
(define-fun _21 () Bool (= _19 _20))
(define-fun _22 () Real 1)
(define-fun _23 () Real |main::d1@2|)
(define-fun _24 () Bool (= _23 _22))
(define-fun _25 () Bool (and _21 _24))
(define-fun _26 () Bool (and _18 _25))
(define-fun _27 () Real |__ADDRESS_OF_main::d2|)
(define-fun _28 () Real (__BASE_ADDRESS_OF__ _27))
(define-fun _29 () Bool (= _27 _28))
(define-fun _30 () Real |main::d2@2|)
(define-fun _31 () Bool (= _30 _22))
(define-fun _32 () Bool (and _29 _31))
(define-fun _33 () Bool (and _26 _32))
(define-fun _34 () Real |__ADDRESS_OF_main::d3|)
(define-fun _35 () Real (__BASE_ADDRESS_OF__ _34))
(define-fun _36 () Bool (= _34 _35))
(define-fun _37 () Real |main::d3@2|)
(define-fun _38 () Bool (= _37 _22))
(define-fun _39 () Bool (and _36 _38))
(define-fun _40 () Bool (and _33 _39))
(define-fun _41 () Real |__ADDRESS_OF_main::c1|)
(define-fun _42 () Real (__BASE_ADDRESS_OF__ _41))
(define-fun _43 () Bool (= _41 _42))
(define-fun _44 () Bool (and _40 _43))
(define-fun _45 () Real |__ADDRESS_OF_main::c2|)
(define-fun _46 () Real (__BASE_ADDRESS_OF__ _45))
(define-fun _47 () Bool (= _45 _46))
(define-fun _48 () Bool (and _44 _47))
(define-fun _49 () Real |main::x1@3|)
(define-fun _50 () Bool (<= _49 _7))
(define-fun _51 () Bool (not _50))
(define-fun _53 () Bool (and _48 _51))
(define-fun _54 () Bool (and _48 _50))
(define-fun _55 () Real |main::x2@3|)
(define-fun _56 () Bool (<= _55 _7))
(define-fun _57 () Bool (not _56))
(define-fun _59 () Bool (and _53 _57))
(define-fun _60 () Bool (and _53 _56))
(define-fun _61 () Bool (or _54 _60))
(define-fun _62 () Real |main::x3@3|)
(define-fun _63 () Bool (<= _62 _7))
(define-fun _67 () Bool (and _59 _63))
(define-fun _68 () Bool (or _61 _67))
(define-fun _69 () Real |__ADDRESS_OF_main::__CPAchecker_TMP_0|)
(define-fun _70 () Real (__BASE_ADDRESS_OF__ _69))
(define-fun _71 () Bool (= _69 _70))
(define-fun _72 () Bool (and _68 _71))
(define-fun _73 () Bool (= _49 _7))
(define-fun _75 () Bool (and _72 _73))
(define-fun _76 () Bool (not _73))
(define-fun _77 () Bool (and _72 _76))
(define-fun _78 () Bool (= _55 _7))
(define-fun _80 () Bool (and _77 _78))
(define-fun _81 () Bool (not _78))
(define-fun _82 () Bool (and _77 _81))
(define-fun _83 () Bool (or _75 _80))
(define-fun _84 () Bool (= _62 _7))
(define-fun _86 () Bool (and _82 _84))
(define-fun _87 () Bool (not _84))
(define-fun _88 () Bool (and _82 _87))
(define-fun _89 () Bool (or _83 _86))
(define-fun _90 () Real |main::__CPAchecker_TMP_0@3|)
(define-fun _91 () Bool (= _90 _7))
(define-fun _92 () Bool (and _88 _91))
(define-fun _93 () Bool (= _90 _22))
(define-fun _94 () Bool (and _89 _93))
(define-fun _95 () Bool (or _92 _94))
(define-fun _96 () Real |__VERIFIER_assert::cond@2|)
(define-fun _97 () Bool (= _90 _96))
(define-fun _98 () Bool (and _95 _97))
(define-fun _99 () Bool (= _96 _7))
(define-fun _101 () Bool (and _98 _99))
(declare-fun __ART__34@0 () Bool)
(declare-fun |main::c2@3| () Real)
(declare-fun __ART__24@0 () Bool)
(declare-fun __ART__45@0 () Bool)
(declare-fun |main::c1@3| () Real)
(declare-fun __ART__23@0 () Bool)
(declare-fun __ART__32@0 () Bool)
(declare-fun __ART__36@0 () Bool)
(declare-fun __ART__26@0 () Bool)
(declare-fun __ART__53@0 () Bool)
(declare-fun __ART__29@0 () Bool)
(define-fun _64 () Bool (not _63))
(define-fun _108 () Real |main::c1@3|)
(define-fun _109 () Bool (= _108 _7))
(define-fun _123 () Real |main::c2@3|)
(define-fun _124 () Bool (= _123 _7))
(define-fun _160 () Bool __ART__23@0)
(define-fun _161 () Bool (= _51 _160))
(define-fun _162 () Bool __ART__24@0)
(define-fun _163 () Bool (= _57 _162))
(define-fun _164 () Bool (and _161 _163))
(define-fun _165 () Bool __ART__26@0)
(define-fun _166 () Bool (= _64 _165))
(define-fun _167 () Bool (and _164 _166))
(define-fun _168 () Bool __ART__29@0)
(define-fun _169 () Bool (= _109 _168))
(define-fun _170 () Bool (and _167 _169))
(define-fun _171 () Bool __ART__32@0)
(define-fun _172 () Bool (= _73 _171))
(define-fun _173 () Bool (and _170 _172))
(define-fun _174 () Bool __ART__34@0)
(define-fun _175 () Bool (= _78 _174))
(define-fun _176 () Bool (and _173 _175))
(define-fun _177 () Bool __ART__36@0)
(define-fun _178 () Bool (= _84 _177))
(define-fun _179 () Bool (and _176 _178))
(define-fun _180 () Bool __ART__45@0)
(define-fun _181 () Bool (= _99 _180))
(define-fun _182 () Bool (and _179 _181))
(define-fun _183 () Bool __ART__53@0)
(define-fun _184 () Bool (= _124 _183))
(define-fun _185 () Bool (and _182 _184))


(push 1)
(assert _101)
(set-info :status sat)
(check-sat)
(push 1)
(assert _185)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
(exit)