Greetings,
the question is
how deep does Z3 considers c#+spec# code paths when verifying it?
that is - are method constraints (''ensures'' for example) verified within the method they are declared in, considering external function calls using only their pre- and post- conditions? Or these external functions are also considered in detail (including possible execution paths)
or within a module, when dealing with, for example, class invariants:
does Z3 verifies class invariants within the module scope using constraints for description of interaction with external modules? Or it uses the full system (program) description to verify any property?
This is in fact determined by how Boogie generates verification conditions. You can view the verification conditions by passing in flags to Boogie/Spec# that dump the formulas that get passed in to Z3 to a text file. These text files can be hard to read, but should have a sufficient overlap of keywords from your original program so you can see what happens. There are also a number of papers that describe the verification condition generator used in Spec#/Boogie. Z3 just verifies (or tries to verify) whatever formula it is given. It does not extract verification conditions from programs, this is done b y the Boogie tool.
Hope this helps