Dafny: another issue with sets

Oct 16, 2012 at 2:27 PM

I use sets with different type parameters : http://rise4fun.com/Dafny/2XC3 . I wonder why Dafny can't prove LemmaInt (and LemmaInt2 which has additional assertions) but it can prove LemmaT.  These lemmas are the same except the type parameter of sets. May be this issue concern with boxing feature of Dafny or this issue is a kind of a "bug" ?

Oct 16, 2012 at 2:38 PM

I have found a workaround of this issue -- it is enough just to call LemmaT with arguments of LemmaInt ( http://rise4fun.com/Dafny/R0Sf ). But I think this solution isn't good enough to leave the issue without concerning.

Oct 17, 2012 at 10:29 PM

Now fixed.  See http://boogie.codeplex.com/discussions/398658.