Invalid model on float formula

Z3Prover / z3

The Z3 Theorem Prover

Other

10k stars 1.46k forks source link

Invalid model on float formula #7162

Open wintered opened 4 months ago

wintered commented 4 months ago

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 commented 4 months ago

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

wintered commented 4 months ago

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