Fix bvAshr shift value to be unsigned

[kquick]

Currently, the bvAshr shift value is treated as a signed value, resulting in a shift left if the shift value is negative.

From SMTLib theory:

    (bvashr s t) abbreviates
            (ite (= ((_ extract |m-1| |m-1|) s) # b0)
                 (bvlshr s t)
                 (bvnot (bvlshr (bvnot s) t)))

[space added after the # character above because of github issue/pr completion]

This indicates that the shift amount for bvAshr should changed to always be treated as unsigned, which matches the handling of bvLshr and bvShlas well as the bvRor and bvRol operations.

[robdockins]

The relevant code appears to be in What4.Expr.Builder:

  bvAshr sym x y
   | Just i <- asSignedBV x, Just n <- asSignedBV y = do
     bvLit sym (bvWidth x) $ Bits.shiftR i (fromIntegral n)
   | Just 0 <- asUnsignedBV y = do
     pure x
   | otherwise = do
     sbMakeExpr sym $ BVAshr (bvWidth x) x y

In the first clause, the shift amount n should be treated as unsigned. And, as with #432, there should be tests for shifting more than bvWidth.

[kquick]

Fixed by #450