aut.is_empty() does not return a counterexample
aut.is_empty() only return a boolean. It should be better if it can return an object where we can ask for the counterexample (if exists). Nonetheless since if (aut.is_empty()) is very useful the return object must be able to destroy every thing related to the emptiness check.