summaryrefslogtreecommitdiff
path: root/Source/Dafny/Translator.cs
diff options
context:
space:
mode:
authorGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-07-28 18:07:23 -0700
committerGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-07-28 18:07:23 -0700
commitfe6ba192bd4430f27e4379c584fbc082bf49be18 (patch)
treedeba25e84b3ff9bd5e5c63619368267d3c016927 /Source/Dafny/Translator.cs
parent1258fd132d80cfdba5e59cfd76c517a091269d2d (diff)
parent3cfa0049262a9d547f061937d5c452afb2033401 (diff)
Merge
Diffstat (limited to 'Source/Dafny/Translator.cs')
-rw-r--r--Source/Dafny/Translator.cs7
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 {