Change dhcp_num_option() to return the numerical value directly.