0

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)?

Improve this question

1 Answer 1

Reset to default
2

Yea, that's the behavior currently which I agree can be confusing. We'll soon add successful properties to the report too.

Improve this answer
3
  • Looks like your recent PR 13957 has addressed this issue? If yes, will this be included in Solidity v0.8.20?
    – Paul Razvan Berg
    Commented Mar 19, 2023 at 13:48
  • 1
    Yes, exactly! It's already available in the nightlies if you wanna play with it, and it'll be part of the next release.
    – Leonardo Alt
    Commented Mar 20, 2023 at 18:34
  • Good stuff, thanks for confirming.
    – Paul Razvan Berg
    Commented Mar 21, 2023 at 11:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.