Function encode_expr_int 

pub fn encode_expr_int(
    expr: &VerifyExpr,
    int_vars: &HashMap<String, Int>,
) -> Option<Int>

Try to encode an expression as a Z3 Int. Returns None if not integer-typed.