Error handling for BitVec of size around 2**32

[yakymp]

I am new to Z3 and accidentally called BitVec(foo, 2**bar) instead of BitVec(foo, bar). Two observations:

1. Calling BitVec(foo, 2**32-1) crashes my Python kernel.
2. Using 2**32 - 2 or 2**32 results in two different error messages.

import z3
errs = set()
for i in range(66):
    try:
        z3.BitVec('foo', 2**i)
    except Exception as e:
        se = str(e)
        if se not in errs:
            errs.add(se)
            print(f"{i} 2**{i} {e}")

print( z3.get_full_version() )

# 29 2**29 b'Overflow encountered when expanding vector'
# 32 2**32 b'bit-vector size must be greater than zero'
# Z3 4.13.3.0