Newlib-BadKrozingenChallenge-Oversimplified-sfxp_16.16_RD_ST.smt2

(set-info :smt-lib-version 2.6)
(set-logic QF_FXP)
(set-info :source | Generated by: Matthias Heizmann Generated on: May 2017 Generator: Ultimate Automizer https://ultimate.informatik.uni-freiburg.de/automizer/ Application: Verification of the Newlib C library |)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status sat)
(declare-fun ~qS4_-1 () (_ SFXP 32 16))
(declare-fun |__ieee754_acos_#in~x_-1| () (_ SFXP 32 16))
(declare-fun ~qS3_-1 () (_ SFXP 32 16))
(declare-fun ~qS2_-1 () (_ SFXP 32 16))
(declare-fun ~pS3_-1 () (_ SFXP 32 16))
(declare-fun ~pS4_-1 () (_ SFXP 32 16))
(declare-fun ~pS5_-1 () (_ SFXP 32 16))
(declare-fun ~pS0_-1 () (_ SFXP 32 16))
(declare-fun ~pS1_-1 () (_ SFXP 32 16))
(declare-fun ~pS2_-1 () (_ SFXP 32 16))
(declare-fun ~qS1_-1 () (_ SFXP 32 16))
(declare-fun ~one_-1 () (_ SFXP 32 16))
(declare-fun __ieee754_acos_~z~1_0 () (_ SFXP 32 16))
(declare-fun __ieee754_acos_~x_0 () (_ SFXP 32 16))
(declare-fun __ieee754_acos_~q~1_0 () (_ SFXP 32 16))
(declare-fun __ieee754_acos_~p~1_0 () (_ SFXP 32 16))
(assert (= __ieee754_acos_~x_0 |__ieee754_acos_#in~x_-1|))
(assert (= __ieee754_acos_~z~1_0 (sfxp.mul saturation roundDown __ieee754_acos_~x_0 __ieee754_acos_~x_0)))
(assert (= __ieee754_acos_~p~1_0 (sfxp.mul saturation roundDown __ieee754_acos_~z~1_0 (sfxp.add saturation ~pS0_-1 (sfxp.mul saturation roundDown __ieee754_acos_~z~1_0 (sfxp.add saturation ~pS1_-1 (sfxp.mul saturation roundDown __ieee754_acos_~z~1_0 (sfxp.add saturation ~pS2_-1 (sfxp.mul saturation roundDown __ieee754_acos_~z~1_0 (sfxp.add saturation ~pS3_-1 (sfxp.mul saturation roundDown __ieee754_acos_~z~1_0 (sfxp.add saturation ~pS4_-1 (sfxp.mul saturation roundDown __ieee754_acos_~z~1_0 ~pS5_-1)))))))))))))
(assert (= __ieee754_acos_~q~1_0 (sfxp.add saturation ~one_-1 (sfxp.mul saturation roundDown __ieee754_acos_~z~1_0 (sfxp.add saturation ~qS1_-1 (sfxp.mul saturation roundDown __ieee754_acos_~z~1_0 (sfxp.add saturation ~qS2_-1 (sfxp.mul saturation roundDown __ieee754_acos_~z~1_0 (sfxp.add saturation ~qS3_-1 (sfxp.mul saturation roundDown __ieee754_acos_~z~1_0 ~qS4_-1))))))))))
(assert (= __ieee754_acos_~q~1_0 ((_ sfxp 16) #x00000000)))
(check-sat)
(exit)