Invalid model on float formula

[wintered]

trafficstars

0b3bbc297248849cb17c29e0fbaa23f61bb45716

$z3release model_validate=true bug.smt2
sat
(error "line 7 column 12: an invalid model was generated")
$cat bug.smt2 
( declare-const a0 (_ FloatingPoint 11 53) ) 
( declare-const a1 (_ FloatingPoint 11 53) ) 
( declare-const a3 (_ FloatingPoint 11 53) ) 
( declare-const a4 (_ FloatingPoint 11 53) ) 
( assert ( = (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) 
( fp.sub RNA a4 ( fp.fma RTN a3 a1 a0 ) ) ) ) 
( check-sat )
$

[benjaminfjones]

@wintered Is the commit you linked to at the top the point you've bisected the issue to?

[wintered]

@benjaminfjones no above link is not the commit I bisected to. It is the commit where the bug triggers.