diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2013-01-21 16:44:19 -0800 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2013-01-21 16:44:19 -0800 |
| commit | 5a0275bc5fe3f8450501ddaac8e464bf0b445804 (patch) | |
| tree | 7cfda1bda6d02d0be71cdc56bda13574d9d0544a /Source/Dafny | |
| parent | 6b2e7f0b312cce4bf6eb3935c51fcb3bc7b4d957 (diff) | |
Fixed bug in translation
Diffstat (limited to 'Source/Dafny')
| -rw-r--r-- | Source/Dafny/Translator.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 67a4aee0..cb43edbc 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1762,7 +1762,7 @@ namespace Microsoft.Dafny { moreBvs.AddRange(bvs);
moreBvs.Add(k);
var z = Bpl.Expr.Eq(kId, Bpl.Expr.Literal(0));
- funcID = new Bpl.IdentifierExpr(tok, FunctionName(pp, 0), TrType(pp.ResultType));
+ funcID = new Bpl.IdentifierExpr(tok, FunctionName(pp, pp.IsRecursive ? 0 : 1), TrType(pp.ResultType));
var prefixLimited = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(funcID), prefixArgs);
var trueAtZero = new Bpl.ForallExpr(tok, moreBvs, BplImp(BplAnd(ante, z), prefixLimited));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(tok, trueAtZero));
|