I called those out as not practical problems because the commenter specifically asked for that. I’m all for research, but there’s this bait and switch that goes on with SMT solvers. They’re presented as useful (TFA says “underused”) and when someone asks for real life use cases, people show minesweeper.