distinct doesn't handle floats

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

243 stars 34 forks source link

distinct doesn't handle floats #592

Closed LeventErkok closed 3 years ago

LeventErkok commented 3 years ago

*Main> sat $ \x -> distinct [x::SDouble,x,x]
*** Exception: SBV.SMTLib2.sh.lift2: Unexpected arguments: ("fp.eq",["s0","s0","s0"])
CallStack (from HasCallStack):
  error, called at ./Data/SBV/SMT/SMTLib2.hs:727:29 in sbv-8.16.5-inplace:Data.SBV.SMT.SMTLib2

It handles correctly if the list has <= 2 elements, but not for more.