This example shows how to use getters in combination with the witness encoding of predicates with arguments. When calling the tool on this file, the verification result should be a _Pass_.
|Path to example file||witnesses/Getters.java|
|Lines of code||58 lines (comments not included)|
|Lines of specification||32 lines (55.17% of the total)|
Note, verification may take a while and has a time-out of 20 seconds.