Summary: A node is not processed in dump_nodes() if it was visited during processing previous inputs. Reviewed-by: rasbold