diff options
| author |  Unknown <leino@leino5.redmond.corp.microsoft.com> | 2011-04-04 18:45:15 -0700 |
|---|---|---|
| committer | Unknown <leino@leino5.redmond.corp.microsoft.com> | 2011-04-04 18:45:15 -0700 |
| commit | fbb1ee30ae5b6e2335eb7af7ebb9a83b7c696289 (patch) | |
| tree | e9d6033afdd497dd5dda5c09d4119c87b4fa14ca /Source | |
| parent | 2b09756f836307f75a36c5a982784dc620fda657 (diff) | |
Dafny: fixed bug in induction over integers
Dafny: added pow2 example
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Translator.cs | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index ab9616b9..f9d152b7 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -5143,9 +5143,11 @@ namespace Microsoft.Dafny { foreach (var n in inductionVariables) {
var newCases = new List<Bpl.Expr>();
foreach (var kase in InductionCases(n.Type, nn[i], etran)) {
- if (kase != Bpl.Expr.True) { // if there's no case, don't add anything to the token
- foreach (var cs in caseProduct) {
+ foreach (var cs in caseProduct) {
+ if (kase != Bpl.Expr.True) { // if there's no case, don't add anything to the token
newCases.Add(Bpl.Expr.Binary(new NestedToken(cs.tok, kase.tok), Bpl.BinaryOperator.Opcode.And, cs, kase));
+ } else {
+ newCases.Add(cs);
}
}
}
|