Added nonlinear example
Quote IDs as needed for SMT-LIB2