Lightweight set solver tactic?
Hello,
Within some custom tactic, I sometimes invoke set_solver on goals that are not directly solvable with set_solver. In that case set_solver can take a long time or diverge, and this slows down the whole tactic. Instead I would like set_solver to fail quickly, so that the custom tactic can try other things. Is there a lightweight solver that would fail early in cases where it is not able to solve the goal?
(Sorry for not providing an example, I can give one if that helps)
Thank you