search

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
239 stars 33 forks source link

CFP case missing in the Eq instance for CVal #699

Closed lsrcz closed 2 months ago

lsrcz commented 2 months ago

Here is the code.

https://github.com/LeventErkok/sbv/blob/82c3df396d86bce47a193db649a34655275dfff2/Data/SBV/Core/Concrete.hs#L112-L134

I am unsure whether doing fprCompareObject a b == EQ is appropriate here as I am not familiar with how this part of the codebase is handling +/-0 and NaNs. Do you have any suggestions?

LeventErkok commented 2 months ago

yeah; that piece of code looks problematic. Let me take a look..

LeventErkok commented 2 months ago

OK, I pushed a commit that should address the missing case and fix that code up to be more robust.

I'll leave this ticket open till you get around to trying it out and it at least works for you. Good find!

LeventErkok commented 2 months ago

Use this commit (or later) to test: https://github.com/LeventErkok/sbv/commit/190ea1481d6eec70181ed000b4605cba7c218e85

lsrcz commented 2 months ago

Hi @LeventErkok, thanks, I think this works.

LeventErkok commented 2 months ago

Great!