To develop a robotic system that will be able to accomplish high-level tasks specifications considering high-dimensional and nonlinear dynamics in the face of uncertain, unanticipated, and dynamically changing situations. The goal is to design autonomous robots for manipulation tasks which are able to work cooperatively in warehouses, housekeeping, and other robot assistant applications. In order to achieve this, we leverage modern Satisfiability Modulo Theories (SMT) solvers and trajectory synthesis techniques. Our basic idea is a counterexample-guided synthesis which combines logic inference with optimization to easy the computation due non-convexities from logic constraints.