mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 03:05:31 -05:00
112 lines
4.3 KiB
Text
112 lines
4.3 KiB
Text
(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)
|