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
smime.p7s
Description: S/MIME cryptographic signature
____________________ Racket Users list: http://lists.racket-lang.org/users
