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

; 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