[racket] Experience with SMT solvers for test generation?

Does anyone on this list have experience with SMT solvers and their use in test-generation tools like DART and SAGE? I have a student that's interested in this stuff, and it looks to me like most of the existing SMT solvers focus on theories of arithmetic, rather than structured values. I have a faint sense that what SMT solvers call "empty theory" may in fact suffice for the kinds of things I have in mind, but I'd like to hear from someone who knows more about it.

Thanks in advance!

John

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4800 bytes
Desc: not available
URL: <http://lists.racket-lang.org/users/archive/attachments/20120620/17874680/attachment.p7s>