1 files changed, 168 insertions, 0 deletions
diff --git a/test/regress/regress1/bug800.smt2 b/test/regress/regress1/bug800.smt2
new file mode 100644
index 000000000..d36f62b16
--- /dev/null
+++ b/test/regress/regress1/bug800.smt2
@@ -0,0 +1,168 @@
+; 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)