I have not solved the problems, but I understand it is only a contingent problem that will be resolved in due course.
The z3.1 tool works, and can handle most situations, all or most of the class commands (object invariants, [Additive], expose, [Rep], [Peer] etc.).
There are issues using the product comprehension, and often multiplying two variables in e.g. an invariant.
However, the Simplify verifier seems to handle many, but not all, of these issues, as the tools stand.
There are instructions about installing Simplify here:
You can use it like this: sscboogie file.exe /prover:Simplify
Also, you can append /simplifyMatchDepth:5, or another integer, and this will sometimes encourage the prover enough to return a positive.
However z3.1 still works best in most circumstances.
I also use Visual Studio 2010 at home, and cannot use the as-you-code Visual Studio 2008 features.
However I find the VS command line works well - I just save textfiles from VS as .ssc.
Hope some of that helps,