-
Notifications
You must be signed in to change notification settings - Fork 0
/
Newlib-BadKrozingenChallenge-Oversimplified-sfxp_16.16_RU_ST.smt2
29 lines (29 loc) · 2.17 KB
/
Newlib-BadKrozingenChallenge-Oversimplified-sfxp_16.16_RU_ST.smt2
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
(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 roundUp __ieee754_acos_~x_0 __ieee754_acos_~x_0)))
(assert (= __ieee754_acos_~p~1_0 (sfxp.mul saturation roundUp __ieee754_acos_~z~1_0 (sfxp.add saturation ~pS0_-1 (sfxp.mul saturation roundUp __ieee754_acos_~z~1_0 (sfxp.add saturation ~pS1_-1 (sfxp.mul saturation roundUp __ieee754_acos_~z~1_0 (sfxp.add saturation ~pS2_-1 (sfxp.mul saturation roundUp __ieee754_acos_~z~1_0 (sfxp.add saturation ~pS3_-1 (sfxp.mul saturation roundUp __ieee754_acos_~z~1_0 (sfxp.add saturation ~pS4_-1 (sfxp.mul saturation roundUp __ieee754_acos_~z~1_0 ~pS5_-1)))))))))))))
(assert (= __ieee754_acos_~q~1_0 (sfxp.add saturation ~one_-1 (sfxp.mul saturation roundUp __ieee754_acos_~z~1_0 (sfxp.add saturation ~qS1_-1 (sfxp.mul saturation roundUp __ieee754_acos_~z~1_0 (sfxp.add saturation ~qS2_-1 (sfxp.mul saturation roundUp __ieee754_acos_~z~1_0 (sfxp.add saturation ~qS3_-1 (sfxp.mul saturation roundUp __ieee754_acos_~z~1_0 ~qS4_-1))))))))))
(assert (= __ieee754_acos_~q~1_0 ((_ sfxp 16) #x00000000)))
(check-sat)
(exit)