Skeleton statement matching issue

Dec 14, 2012 at 9:03 PM

I use Dafny 2.2.40819.0703. It says "max.dfy(39,3): Error: skeleton statement may not be used here; it does not have a matching statement in what is being replaced" and raises an exception:

"

Unhandled Exception: System.Diagnostics.Contracts.__ContractsRuntime+ContractException: Precondition failed: WasResolved()   at System.Diagnostics.Contracts.__ContractsRuntime.TriggerFailure(ContractFailureKind kind, String msg, String userMessage, String conditionTxt, Exception inner) in :line 0   at System.Diagnostics.Contracts.__ContractsRuntime.ReportFailure(ContractFailureKind kind, String msg, String conditionTxt, Exception inner) in :line 0   at System.Diagnostics.Contracts.__ContractsRuntime.Requires(Boolean condition, String msg, String conditionTxt) in :line 0   at Microsoft.Dafny.Expression.get_Resolved() in D:\Temp\aste\Boogie\Source\Dafny\DafnyAst.cs:line 2822   at Microsoft.Dafny.RefinementTransformer.CheckIsOkayUpdateStmt(ConcreteUpdateStatement stmt, ModuleDefinition m, ResolutionErrorReporter reporter) in D:\Temp\aste\Boogie\Source\Dafny\RefinementTransformer.cs:line 1229   at Microsoft.Dafny.RefinementTransformer.<>c__DisplayClassd.<CheckIsOkayNewStatement>b__b() in D:\Temp\aste\Boogie\Source\Dafny\RefinementTransformer.cs:line 1205   at Microsoft.Dafny.RefinementTransformer.PostResolve(ModuleDefinition m) in D:\Temp\aste\Boogie\Source\Dafny\RefinementTransformer.cs:line 450   at Microsoft.Dafny.Resolver.ResolveProgram(Program prog) in D:\Temp\aste\Boogie\Source\Dafny\Resolver.cs:line 212   at Microsoft.Dafny.Main.ParseCheck(List`1 fileNames, String programName, Program& program) in D:\Temp\aste\Boogie\Source\Dafny\DafnyMain.cs:line 68   at Microsoft.Dafny.DafnyDriver.ProcessFiles(List`1 fileNames) in D:\Temp\aste\Boogie\Source\DafnyDriver\DafnyDriver.cs:line 149   at Microsoft.Dafny.DafnyDriver.Main(String[] args) in D:\Temp\aste\Boogie\Source\DafnyDriver\DafnyDriver.cs:line 85

"

for the following program: http://rise4fun.com/Dafny/ULfW .  How should I use skeletons right ?