diff options
| author |  Rustan Leino <unknown> | 2015-07-24 20:49:43 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2015-07-24 20:49:43 -0700 |
| commit | 1ca106492d5680c29bfa83b34ff79f7ff8407db7 (patch) | |
| tree | 58f82b375f2c754c876b589d2c00573cd1626115 /Source | |
| parent | 8a26fae8810b3a0419df1704de2b23926b95e92e (diff) | |
Translate triggers with the same ExpressionTranslator as the body
Signed-off-by: Clement Pit--Claudel <clement.pitclaudel@live.com>
Diffstat (limited to 'Source')
| -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 05633742..3821e5df 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) {
@@ -13039,9 +13039,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 {
|