diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-17 09:37:47 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-17 09:37:47 -0700 |
| commit | db9821ac440cdfa817049ab83c2e94f861ff429d (patch) | |
| tree | cfbb6ed0d116f764474ba4e07c4b406fa6916e4a /Source/Dafny/Cloner.cs | |
| parent | a07b43ac03b38d4af575d1a1df48339ad228751a (diff) | |
Review preceding commit with Rustan
Diffstat (limited to 'Source/Dafny/Cloner.cs')
| -rw-r--r-- | Source/Dafny/Cloner.cs | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 961d4d14..e89a385f 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -374,18 +374,13 @@ namespace Microsoft.Dafny if (e is QuantifierExpr) {
var q = (QuantifierExpr)e;
var tvs = q.TypeArgs.ConvertAll(CloneTypeParam);
- QuantifierExpr cloned;
if (e is ForallExpr) {
- cloned = new ForallExpr(tk, tvs, bvs, range, term, CloneAttributes(e.Attributes));
+ return new ForallExpr(tk, tvs, bvs, range, term, CloneAttributes(e.Attributes));
} else if (e is ExistsExpr) {
- cloned = new ExistsExpr(tk, tvs, bvs, range, term, CloneAttributes(e.Attributes));
+ return new ExistsExpr(tk, tvs, bvs, range, term, CloneAttributes(e.Attributes));
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected quantifier expression
}
- if (q.SplitQuantifier != null) { //TODO CLEMENT TRIGGERS: Should we clone the quantifier as a quantifier in this case? Or should we just replace entirely?
- cloned.SplitQuantifier = q.SplitQuantifier.Select(CloneExpr).ToList();
- }
- return cloned;
} else if (e is MapComprehension) {
return new MapComprehension(tk, ((MapComprehension)e).Finite, bvs, range, term, CloneAttributes(e.Attributes));
} else if (e is LambdaExpr) {
|