Overflow-safe BitVec

[bruderj15]

Currently we can easily do polymorph definitions of problems like:

problem  :: (Orderable (Expr t), Num (Expr t)) => ... -> Expr BoolSort
problem = ...

main :: IO ()
main = do
  solveWith @SMT (solver z3) $ problem @RealSort
  solveWith @SMT (solver z3) $ problem @IntSort ...
  solveWith @SMT (solver z3) $ problem @(BvSort Unsigned 8) ...

This works fine for IntSort and RealSort. However one needs to deal with overflow for fixed size bv of size n: BvSort _ n. Currently in use cases I encode extra overflow contraints via checking t with KnownSMTSort t inside problem.

That is bad.

Add an overflow-safe BitVec type. Ideally some wrapper and not a new sort.

[bruderj15]

Some solvers like Z3 have special operations therefore. Is that general enough?