A symbolic compiler translates a program to symbolic constraints, automatically reducing model checking and program synthesis to constraint solving. Symbolic compilers are versatile tools: during the last decade, a small number of symbolic compilers enabled automatic construction of many synthesizers for domains ranging from programming by demonstration to inference of memory models. New applications of constraint solvers will however require orders-of-magnitude improvements in solving efficiency. The good news is that these improvements can be delivered with today’s solvers by simply encoding programs more cleverly, with in domain-specific constraints. Unfortunately, today’s symbolic compilers cannot translate programs to these special encodings, forcing us to write constraint generators, which are error-prone and must be developed for each problem anew.To trick symbolic compilers into producing efficient constraints, we have introduced so-called symbolic abstractions. These abstractions hide the domain-specific encoding yet they behave as their non-symbolic counterparts — programmers can keep conveniently writing code using these abstractions, as well as test and debug their programs on concrete inputs. Yet when programs built from these abstractions are symbolically compiled, the desired constraints are produced.I will demonstrate the idea by developing the first non-fuzzing checker of type systems; by automatically turning a spatial type checker into a partitioner that maps a program onto a many-core accelerator; and by producing a parallelizer of attribute grammar evaluators.