This verification example passes, but produces a Silver warning that "abstract predicates cannot be (un)folded". VerCors does however not report this error.
|Path to example file||known-problems/FunctionProblem.pvl|
|Lines of code||12 lines (comments not included)|
|Lines of specification||5 lines (41.67% of the total)|
|Computation time||17104 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.