# Total number of time an already memorized node is seen again.
	# If `memorize_late` is set, then only visited nodes are counted.
	# Otherwise, nodes in the todo-list are also considered.
	var memorized = 0