test: add more regression files

tests/sat/cpachecker-induction.1_3.c_false-unreach-call.i.smt2

@@ -0,0 +1,112 @@
+(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 sat)
+
+
+(declare-fun |freePtr::ptr@3| () Real)
+(declare-fun *signed_int@4 (Real) Real)
+(declare-fun |getrr::__CPAchecker_TMP_0@3| () Real)
+(declare-fun |getrr::r@2| () Real)
+(declare-fun __BASE_ADDRESS_OF__ (Real) Real)
+(declare-fun *signed_int@3 (Real) Real)
+(declare-fun |__ADDRESS_OF_main::ptr1| () Real)
+(declare-fun |malloc#2| () Real)
+(declare-fun |__ADDRESS_OF_getPtr::r| () Real)
+(declare-fun |freePtr::ptr@2| () Real)
+(declare-fun |__ADDRESS_OF_getrr::__CPAchecker_TMP_0| () Real)
+(declare-fun |main::ptr1@2| () Real)
+(declare-fun *signed_int@2 (Real) Real)
+(declare-fun |__ADDRESS_OF___VERIFIER_successful_alloc_*void#1| () Real)
+(declare-fun |__ADDRESS_OF_getrr::r| () Real)
+(declare-fun |getPtr::__retval__@2| () Real)
+(declare-fun |main::ptr1@3| () Real)
+(declare-fun |getrr::__retval__@2| () Real)
+(declare-fun |getPtr::r@3| () Real)
+(define-fun _7 () Real 0)
+(define-fun _8 () Real |__ADDRESS_OF_main::ptr1|)
+(define-fun _9 () Real (__BASE_ADDRESS_OF__ _8))
+(define-fun _10 () Bool (= _8 _9))
+(define-fun _11 () Real |main::ptr1@2|)
+(define-fun _12 () Bool (= _11 _7))
+(define-fun _13 () Bool (and _10 _12))
+(define-fun _14 () Real |__ADDRESS_OF_getPtr::r|)
+(define-fun _15 () Real (__BASE_ADDRESS_OF__ _14))
+(define-fun _16 () Bool (= _14 _15))
+(define-fun _17 () Bool (and _13 _16))
+(define-fun _18 () Real |__ADDRESS_OF_getrr::__CPAchecker_TMP_0|)
+(define-fun _19 () Real (__BASE_ADDRESS_OF__ _18))
+(define-fun _20 () Bool (= _18 _19))
+(define-fun _21 () Bool (and _17 _20))
+(define-fun _22 () Real |malloc#2|)
+(define-fun _23 () Bool (= _22 _7))
+(define-fun _24 () Bool (not _23))
+(define-fun _27 () Real |getrr::__CPAchecker_TMP_0@3|)
+(define-fun _30 () Real |__ADDRESS_OF_getrr::r|)
+(define-fun _31 () Real (__BASE_ADDRESS_OF__ _30))
+(define-fun _32 () Bool (= _30 _31))
+(define-fun _35 () Real |getrr::r@2|)
+(define-fun _36 () Bool (= _27 _35))
+(define-fun _40 () Real (*signed_int@2 _35))
+(define-fun _41 () Bool (= _40 _7))
+(define-fun _43 () Real |getrr::__retval__@2|)
+(define-fun _44 () Bool (= _35 _43))
+(define-fun _46 () Real |getPtr::r@3|)
+(define-fun _47 () Bool (= _43 _46))
+(define-fun _49 () Real 1)
+(define-fun _50 () Real (*signed_int@3 _46))
+(define-fun _51 () Bool (= _50 _49))
+(define-fun _59 () Real |getPtr::__retval__@2|)
+(define-fun _60 () Bool (= _46 _59))
+(define-fun _62 () Real |main::ptr1@3|)
+(define-fun _63 () Bool (= _59 _62))
+(define-fun _65 () Real |freePtr::ptr@2|)
+(define-fun _66 () Bool (= _62 _65))
+(define-fun _68 () Real (*signed_int@3 _65))
+(define-fun _69 () Bool (= _68 _49))
+(define-fun _75 () Real 2)
+(define-fun _76 () Real (*signed_int@4 _65))
+(define-fun _77 () Bool (= _76 _75))
+(define-fun _84 () Real |freePtr::ptr@3|)
+(define-fun _85 () Bool (= _62 _84))
+(define-fun _87 () Real (*signed_int@4 _84))
+(define-fun _88 () Bool (= _87 _49))
+(define-fun _91 () Bool (not _88))
+(define-fun _161 () Real |__ADDRESS_OF___VERIFIER_successful_alloc_*void#1|)
+(define-fun _162 () Real (ite _24 _161 _7))
+(define-fun _163 () Bool (= _27 _162))
+(define-fun _164 () Bool (and _21 _163))
+(define-fun _165 () Bool (<= _161 _7))
+(define-fun _166 () Bool (not _165))
+(define-fun _167 () Bool (and _32 _166))
+(define-fun _168 () Bool (and _36 _167))
+(define-fun _169 () Bool (and _164 _168))
+(define-fun _170 () Bool (and _41 _169))
+(define-fun _171 () Bool (and _44 _170))
+(define-fun _172 () Bool (and _47 _171))
+(define-fun _173 () Bool (= _46 _161))
+(define-fun _174 () Real (*signed_int@3 _161))
+(define-fun _175 () Real (*signed_int@2 _161))
+(define-fun _176 () Bool (= _174 _175))
+(define-fun _177 () Bool (or _173 _176))
+(define-fun _178 () Bool (and _51 _177))
+(define-fun _179 () Bool (and _172 _178))
+(define-fun _180 () Bool (and _60 _179))
+(define-fun _181 () Bool (and _63 _180))
+(define-fun _182 () Bool (and _66 _181))
+(define-fun _183 () Bool (and _69 _182))
+(define-fun _184 () Bool (= _65 _161))
+(define-fun _185 () Real (*signed_int@4 _161))
+(define-fun _186 () Bool (= _174 _185))
+(define-fun _187 () Bool (or _184 _186))
+(define-fun _188 () Bool (and _77 _187))
+(define-fun _189 () Bool (and _183 _188))
+(define-fun _190 () Bool (and _85 _189))
+(define-fun _191 () Bool (and _91 _190))
+
+
+
+(assert _191)
+(check-sat)
+(exit)

tests/sat/polypaver-bench-exp-3d-chunk-0032.smt2

@@ -0,0 +1,27 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_LRA)
+(set-info :source |
+These benchmarks used in the paper:
+
+  Dejan Jovanovic and Leonardo de Moura.  Solving Non-Linear Arithmetic.
+  In IJCAR 2012, published as LNCS volume 7364, pp. 339--354.
+
+The meti-tarski benchmarks are proof obligations extracted from the
+Meti-Tarski project, see:
+
+  B. Akbarpour and L. C. Paulson. MetiTarski: An automatic theorem prover
+  for real-valued special functions. Journal of Automated Reasoning,
+  44(3):175-205, 2010.
+
+Submitted by Dejan Jovanovic for SMT-LIB.
+
+
+|)
+(set-info :category "industrial")
+(set-info :status sat)
+(declare-fun skoZ () Real)
+(declare-fun skoY () Real)
+(declare-fun skoX () Real)
+(assert (let ((?v_0 (* skoX (- 1))) (?v_1 (* skoY (- 1)))) (and (<= (+ ?v_0 ?v_1) skoZ) (and (not (<= skoZ (+ (+ (/ 3 2) ?v_0) ?v_1))) (and (<= skoZ 1) (and (<= skoY 1) (and (<= skoX 1) (and (<= 0 skoZ) (and (<= 0 skoY) (<= 0 skoX))))))))))
+(check-sat)
+(exit)

tests/unsat/reg_uflra.smt2

@@ -0,0 +1,6 @@
+(set-logic QF_UFLRA)
+(set-info :status unsat)
+(declare-fun f0_2 (Real Real) Real)
+(assert (and (not (< (f0_2 (- 0.0 0.0) 0.0) 10)) (< (f0_2 0.0 0.0) 0)))
+(check-sat)
+(exit)