--logic=QF_UF --mode=push-pop