Ah damn, okay. Long functions with a lot of sub calls is a known problem. I've been able to work around some of the issues tried to them by making every function an independent "compile unit." and then solving them each individually in the SMT solver. My experience in contract based programming is still relatively light, I won't lie there. The most I've had to do with contracts was ada, and even then it wasn't much. Everything else has been self enforced in languages without explicit support (and hence no compile time checking.)