Simplify interaction with solver.

It appears that pushing and poping does work as expected
(i.e., it affects both assertions and declarations).

The issue previously was that I was using `(push)` instead of
`(push 1)`.  While Yices rejects the first, CVC4 accepts it,
but it looks like it treats it as `(push 0)`??   Either way,
when we use `(push 1)`, everything seems to work as expected,
so the machinery to emulate this behavior is not needed.
A comment showing a problem with `solverSimplify` and an idea on how to solve it.