Invalid model for QF_FP formula

[rainoftime]

Hi, for the following formula,
z3 3bca1fb

(declare-fun X () (_ FloatingPoint 2 6))
(declare-fun Y () (_ FloatingPoint 2 6))
(declare-fun Z () (_ FloatingPoint 2 6))
(assert (and (= X (fp.add RTZ Y Z)) (= X (fp.div RTZ Y Z)) (= X (fp.roundToIntegral RTZ Y)) (not (= Y Z))))
(check-sat)
(get-model)

./z3 model_validate=true ../delta.out.smt2 
sat
(error "line 5 column 10: an invalid model was generated")
(
  (define-fun Z () (_ FloatingPoint 2 6)
    (fp #b0 #b00 #b00001))
  (define-fun X () (_ FloatingPoint 2 6)
    (fp #b1 #b01 #b00000))
  (define-fun Y () (_ FloatingPoint 2 6)
    (fp #b1 #b01 #b00001))
)

[rainoftime]

note: instances from #2381 use fp.rem, while the formula above does not mention fp.rem

[wintersteiger]

Sorry, I'm confused, what is related? fp.rem is known to be buggy as witnessed by the fact that there's an open issue for it. This bug report doesn't mention fp.rem though.

[rainoftime]

(set-logic QF_FP)
(declare-fun X () (_ FloatingPoint 11 53))
(declare-fun Y () (_ FloatingPoint 9 53))
(assert (fp.lt X (fp #b0 #b10011111111 #x0000000000000)))
(assert (= Y ((_ to_fp 9 53) RNE X)))
(assert (not (distinct Y (_ +oo 9 53))))
(check-sat)