def METHOD_NAME(self, left: z3.ExprRef, op: str) -> z3.ExprRef:
    """Apply z3 unary operation indicated by op."""
    op_to_z3 = {
        "not": z3.Not,
    }
    if op in op_to_z3:
        left = op_to_z3[op](left)
    else:
        raise Z3ParseException(f"Unhandled unary operation {op}.")
    return left