Related, Kaplan, a Scala based constraint language (uses Z3 for solving): http://lara.epfl.ch/~kuncak/papers/KoeksalETAL12ConstraintsC...

The Lara team at EPFL seems to be doing lots of research in this area: http://lara.epfl.ch/w/Start