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

Add support for CVC5 algebraic reals #627

Closed LeventErkok closed 2 years ago

LeventErkok commented 2 years ago

CVC5 now has much better support for algebraic reals; see here: https://github.com/cvc5/cvc5/issues/8898#issuecomment-1187472197

We should implement support for this in SBV when CVC5 is picked as the backend. (Much like we do with z3.)