Add simplification rule for byte lost in >>

Can help for instance to reduce complexity when a word is used as a
shift buffer for bytes.
Add check_concolic_value debug routine

Add some code to check on the fly whether for each newly generated
temporary subformula, the concolic value of the subformula is
satisfiable under the path condition. This kind of check can help
track down places where the path condition is unexpectedly diverging
from the concolic input, or potentially if the formula construction
is making a mistake.

No command line option to enable it yet, since I don't know how
broadly useful it will be. For now, you just need to uncomment it.