try to infer nullity predicate inside update_predicate_tree. Maybe rethink about...