Possible bug in the Dafny -> C# code generation

Oct 3, 2012 at 11:30 PM
Edited Oct 3, 2012 at 11:36 PM

Here is the program:

http://rise4fun.com/Dafny/pDyTu

It seems that it's caused by the second parallel statement.

array.cs(618,27) : error CS0266: Cannot implicitly convert type 'System.Numerics.BigInteger' to 'int'. An explicit conversion exists (are you missing a cast?)

 

The verification part went through just fine, but it seems that Dafny generate incorrect C# code. I'm using Dafny 2.2.40925.1130 (the latest version of binary available on codeplex).

Hope it helps.

Oct 4, 2012 at 8:42 AM

Fixed.  Thanks for the bug report.