SMC: Satisfiability Modulo Convex Optimization