The set_solver tactic roughly calls set_unfold and then performs naive_solver. @jihgfee noticed that set_solver (without tactic argument) calls naive_solver idtac by default. This is somewhat strange since naive_solver (without tactic argument) defaults to naive_solver eauto.
Also @jihgfee found an example where set_solver by idtac (the current default) is much slower than set_solver by eauto.
So I am wondering what's the reason why set_solver uses idtac? Is that just some arbitrary legacy choice, or does it actually improve performance?