[bbcbasic]

I wonder, does Code Contracts use Z3?

[ygra]

Code Contracts are just assertions. Pex can use them though and is built on Z3, iirc.

[bbcbasic]

They seem to be more than assertions. You get warnings at build time and clearly some proving engine must be in use.