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

New overflow predicates #657

Closed LeventErkok closed 9 months ago

LeventErkok commented 1 year ago

SMTLib has adapted new overflow predicates, and z3 implements them:

bvnego
bvuaddo bvsaddo
bvusubo bvssubo
bvumulo bvsmulo
bvsdivo

(Not sure if z3 implements the bvumolo and bvsmulo, need to check.)

We should make sure SBV uses these sanctioned versions when they come out in the new SMTLib document. (Which isn't out yet.)

LeventErkok commented 1 year ago

Waiting till there's an official SMTLib Bitvector logic update. As of mid-2023 this hasn't happened yet.