Make Solve check its own post-condition, to reduce clutter in the