LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
242 stars 34 forks source link

Fix toSFloatingPoint simplification for AlgReal. #718

Closed lsrcz closed 3 months ago

lsrcz commented 3 months ago

We should only simplify it when RNE.

LeventErkok commented 3 months ago

It's an odd bug; not sure why I considered it'd apply in all rounding modes. Bizarre. Good catch!