fix push/pop bugs in optimize context, add example to c++, fix bug in arithemtic bounds axiom addition

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>