diff options
Diffstat (limited to 'Source/Dafny/Compiler.cs')
| -rw-r--r-- | Source/Dafny/Compiler.cs | 31 |
1 files changed, 10 insertions, 21 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index b2dda7de..35f81605 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -653,36 +653,25 @@ namespace Microsoft.Dafny { Contract.Assert(s.Lhss.Count == resolved.Count);
Contract.Assert(s.Rhss.Count == resolved.Count);
var lvalues = new List<string>();
- int i = 0;
- foreach (var lhs in s.Lhss) {
- if (!resolved[i].IsGhost) {
- lvalues.Add(CreateLvalue(lhs, indent));
- }
- i++;
- }
- int N = i;
var rhss = new List<string>();
- i = 0;
- foreach (var rhs in s.Rhss) {
+ for (int i = 0; i < resolved.Count; i++) {
if (!resolved[i].IsGhost) {
- if (rhs is HavocRhs) {
- rhss.Add(null);
- } else {
+ var lhs = s.Lhss[i];
+ var rhs = s.Rhss[i];
+ if (!(rhs is HavocRhs)) {
+ lvalues.Add(CreateLvalue(lhs, indent));
+
string target = "_rhs" + tmpVarCount;
tmpVarCount++;
rhss.Add(target);
TrRhs("var " + target, null, rhs, indent);
}
}
- i++;
}
- Contract.Assert(lvalues.Count == N);
- Contract.Assert(rhss.Count == N);
- for (i = 0; i < N; i++) {
- if (rhss[i] != null) {
- Indent(indent);
- wr.WriteLine("{0} = {1};", lvalues[i], rhss[i]);
- }
+ Contract.Assert(lvalues.Count == rhss.Count);
+ for (int i = 0; i < lvalues.Count; i++) {
+ Indent(indent);
+ wr.WriteLine("{0} = {1};", lvalues[i], rhss[i]);
}
}
|