progress on the reachability logic prover

can you make this comment a little more verbose explaining what the hack is, why it was necessary, and when it can be removed?