[521] % z3release model_validate=true small.smt2
sat
(error "line 8 column 10: an invalid model was generated")
(
 (define-fun c () Float64
  (fp #b0 #b10101000111 #xd42aea2879f2f))
 (define-fun b () Float64
  (fp #b0 #b10101000111 #xd42aea2879f2f))
 (define-fun d () Float64
  (fp #b0 #b00000000000 #xffffffffffdfe))
 (define-fun a () RoundingMode
  roundTowardZero)
)
unsat
[522] % 
[522] % cat small.smt2
(declare-fun a () RoundingMode)
(declare-fun b () Float64)
(declare-fun c () Float64)
(declare-fun d () Float64)
(assert
 (= ((_ to_fp 11 53) a 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000.0)
 c (fp.add a c d) b))
(check-sat)
(get-model)
(reset)
(define-fun c () Float64 (fp #b0 #b10101000111 #xd42aea2879f2f))
(define-fun b () Float64 (fp #b0 #b10101000111 #xd42aea2879f2f))
(define-fun d () Float64 (fp #b0 #b00000000000 #xffffffffffdfe))
(define-fun a () RoundingMode roundTowardZero)
(assert
 (= ((_ to_fp 11 53) a 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000.0)
 c (fp.add a c d) b))
(check-sat)
[523] %