diff options
author | 2015-07-28 18:07:23 -0700 | |
---|---|---|
committer | 2015-07-28 18:07:23 -0700 | |
commit | fe6ba192bd4430f27e4379c584fbc082bf49be18 (patch) | |
tree | deba25e84b3ff9bd5e5c63619368267d3c016927 /Source/Dafny/Translator.cs | |
parent | 1258fd132d80cfdba5e59cfd76c517a091269d2d (diff) | |
parent | 3cfa0049262a9d547f061937d5c452afb2033401 (diff) |
Merge
Diffstat (limited to 'Source/Dafny/Translator.cs')
-rw-r--r-- | Source/Dafny/Translator.cs | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 83078fb5..b8c4b8ec 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -10623,7 +10623,7 @@ namespace Microsoft.Dafny { public ExpressionTranslator WithNoLits() {
Contract.Ensures(Contract.Result<ExpressionTranslator>() != null);
- return new ExpressionTranslator(translator, predef, HeapExpr, This, null, layerInterCluster, layerIntraCluster, modifiesFrame, true);
+ return new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, modifiesFrame, true);
}
public ExpressionTranslator LimitedFunctions(Function applyLimited_CurrentFunction, Bpl.Expr layerArgument) {
@@ -13035,9 +13035,10 @@ namespace Microsoft.Dafny { typeAntecedent = etran.TrBoundVariables(e.BoundVars, bvars);
foreach (var kase in caseProduct) {
var ante = BplAnd(BplAnd(typeAntecedent, ih), kase);
- var bdy = etran.LayerOffset(1).TrExpr(e.LogicalBody());
+ var etranBody = etran.LayerOffset(1);
+ var bdy = etranBody.TrExpr(e.LogicalBody());
Bpl.Expr q;
- var trig = TrTrigger(etran, e.Attributes, expr.tok);
+ var trig = TrTrigger(etranBody, e.Attributes, expr.tok);
if (position) {
q = new Bpl.ForallExpr(kase.tok, bvars, trig, Bpl.Expr.Imp(ante, bdy));
} else {
|