We introduce Trau, an SMT solver for an expressive constraint
language, including word equations, length constraints, context-free
membership queries, and transducer constraints. The satisfiability
problem for such a class of constraints is in general undecidable. The
key idea behind Trau is a technique called flattening, which searches
for satisfying assignments that follow simple patterns. Trau
implements a Counter-Example Guided Abstraction Refinement (CEGAR)
framework which contains both an under- and an over-approximation
module. The a pproximations are refined in an automatic manner by
information flow between the two modules.  The technique implemented
by Trau can handle a rich class of string constraints and has better
performance than state-of-the-art string solvers.