fix counterexamples when using constants
add support for WillNotOverflowSignedAdd(x,y) predicate
Add precondition language with a few operators
add another test by David Menendez