Go through the program and use algebraic simplification and range analysis to try to figure out which assertions are statically true.

Currently implemented by running the simplifier with a special rule that is too expensive to run all the time.