test/regress/regress0/parser/to_fp.smt2


1
2
3
4
5
6
7
8
9
10

; REQUIRES: symfpu
; COMMAND-LINE: --strict-parsing -q
; EXPECT: sat
(set-logic QF_FP)
(declare-fun |c::main::main::3::div@1!0&0#1| () (_ FloatingPoint 8 24))
(assert (not (fp.eq ((_ to_fp 11 53)
                     roundNearestTiesToEven
                     |c::main::main::3::div@1!0&0#1|)
              (fp #b0 #b00000000000 #x0000000000000))))
(check-sat)