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

; REQUIRES: symfpu
; EXPECT: unsat
(set-logic QF_FP)
(declare-fun bv () (_ BitVec 1))
(define-fun x () (_ FloatingPoint 11 53) ((_ to_fp_unsigned 11 53) RNE bv))
(assert (fp.isNaN x))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback