[584] % z3release model_validate=true small.smt2
sat
(
 (define-fun X () (_ FloatingPoint 11 53)
  (fp #b1 #b01011100010 #x83b6fffeff76e))
 (define-fun Y () (_ FloatingPoint 9 53)
  (fp #b1 #b000000000 #x00000003076e0))
)
sat
unsat
[585] % z3debug model_validate=true small.smt2
sat
(error "line 5 column 10: an invalid model was generated")
(
 (define-fun X () (_ FloatingPoint 11 53)
  (fp #b0 #b00000000000 #x0001a2bffffff))
 (define-fun Y () (_ FloatingPoint 9 53)
  (_ +oo 9 53))
)
sat
unsat
[586] % 
[586] % cat small.smt2
(declare-fun X () (_ FloatingPoint 11 53))
(declare-fun Y () (_ FloatingPoint 9 53))
(assert (fp.leq X (fp #b0 #b10011111110 #xFFFFFFFFFFFFF)))
(assert (= Y ((_ to_fp 9 53) RNE X)))
(check-sat)
(get-model)
(reset)
(define-fun X () (_ FloatingPoint 11 53) (fp #b1 #b01011100010 #x83b6fffeff76e))
(define-fun Y () (_ FloatingPoint 9 53) (fp #b1 #b000000000 #x00000003076e0))
(assert (fp.leq X (fp #b0 #b10011111110 #xFFFFFFFFFFFFF)))
(assert (= Y ((_ to_fp 9 53) RNE X)))
(check-sat)
(reset)
(define-fun X () (_ FloatingPoint 11 53) (fp #b0 #b00000000000 #x0001a2bffffff))
(define-fun Y () (_ FloatingPoint 9 53) (_ +oo 9 53))
(assert (fp.leq X (fp #b0 #b10011111110 #xFFFFFFFFFFFFF)))
(assert (= Y ((_ to_fp 9 53) RNE X)))
(check-sat)
[587] %