From the docs:
If there are any unproved targets, the SMTChecker issues one warning stating how many unproved targets there are.
However, the docs don't say anything about the converse, i.e. what happens if the SMTChecker does not find any unproven targets.
Is it that when the build passes successfully and no warnings are printed, that means the SMTChecker proved the contract successfully (i.e. it did not find any unproven targets)?