The max value test in vc_bvConstExprFromInt (c_interface.cpp) is broken. The computation of max_n_bits:
unsigned long long int max_n_bits = 0xFFFFFFFFFFFFFFFFULL >> 64-n_bits;
performs the right shift first, resulting in zero, then subtracts n_bits from that. Since we are dealing with unsigned numbers, the result is a very large unsigned value, which causes the test just below it to succeed when it shouldn't. The attached patch adds parentheses to force the subtraction to be done before the bit shift.