[sevensor]

If you do want to start with SMT though, z3 has quite good bindings. I found it intuitive to use, and its ability to give you answers to very hard problems is like owning a magic wand.