That would at least make this game more strict and perhaps even more difficult.
While trying this out I've encountered several sections where I would have to guess, and that guess cannot be influenced by other unrevealed cells, such as when there's an island in a corner of the map.
In these situations I will need to guess between these two spaces, but since there are still known safe areas on the map, guessing causes me to lose the game.
I can get used to that behavior of course, but it's fairly frustrating. It'd be nice if the guessing exception rules accounted for situations like this. When there are clearings or known mine patterns that separate out discrete smaller map(s), I want to solve the smaller map(s) before I move on.
I'm not sure how hard this is to add to the SAT solver. The formal definition is something like "if for some set of maybe-squares S, no matter what the solutions are to all of the squares outside S, the set of solutions to S is the same, then allow clicking anywhere in S". But that's a combinatorial explosion: just the number of sets S to consider is a factor of 2^#{maybe-squares} . I don't know enough to say if that can be optimized into something sane so that it can be rigorously applied, but a handful of special cases for small unconnected sections of the board would cover most of it.
If you have all of the possible information for that guess already, then yeah.
If there are still some unknowns that you could resolve first to get more information, then guessing should still result in a mine.
I can't think of any situations where it makes a difference, though, other than ones where you rely on the mines-remaining counter.