summaryrefslogtreecommitdiff
path: root/test/regress/regress0/fp/issue5734.smt2
blob: 2ad9ac92121d6705c99c8e582ee52f2f8cdbf59b (plain) 
1
2
3
4
5
6
7

; REQUIRES: symfpu
; EXPECT: sat
(set-logic QF_FP)
(declare-fun a () RoundingMode)
(declare-fun b () (_ FloatingPoint 8 24))
(assert (= b (fp.add a b (fp.add a ((_ to_fp 8 24) a ((_ to_fp 8 24) a 0)) b))))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback