During #366 we had a bug, where the added restarting behavior made some regression tests fail in an unexpected manner.
Some asserts were never reached, so there was unsoundly dead code, but our verify didn't complain at all, but it should definitely have, since there were live constraints that weren't actually satisfied.

Turns out that verify is complete and doesn't check anything about the variables that were queries by solve. Instead it just checks that everything in the solution hashtable holds:

But there is no check that the queried variables are there and that their constraints are (recursively) satisfied all the way up.
With the current check, a solver could simply return an empty hashtable as the solution and since there's nothing to iterate over, verify would be happy with it, despite obviously missing our queried variables.

In a more subtle case (which is what we had), the solution might be a closed subset of the true solution, but be missing some actually reachable parts.

Hence, we need a proper verify must follow the inductive definition of a partial solution w.r.t. the queried variables. This might be a primitive top-down verify, which doesn't need to solve, but just check in demand-driven manner from the queried variables.