diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-04-05 17:18:51 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-04-05 17:18:51 -0700 |
| commit | c382dec32aac64dfa50e999795841950e4d81fed (patch) | |
| tree | c575441e7ec384941177a7a6c846e4f6a5f0a8f8 /Source | |
| parent | 343f29bee9cad726c2de33d4ef6cdb49caa965d2 (diff) | |
| parent | e06dd62cbfe52cb75f358b22a98aadd12b52eb83 (diff) | |
branch merge
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Translator.cs | 6 | ||||
| -rw-r--r-- | Source/ModelViewer/Main.cs | 1 |
2 files changed, 4 insertions, 3 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 708c4c06..33b6d39d 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -5173,9 +5173,11 @@ namespace Microsoft.Dafny { foreach (var n in inductionVariables) {
var newCases = new List<Bpl.Expr>();
foreach (var kase in InductionCases(n.Type, nn[i], etran)) {
- if (kase != Bpl.Expr.True) { // if there's no case, don't add anything to the token
- foreach (var cs in caseProduct) {
+ foreach (var cs in caseProduct) {
+ if (kase != Bpl.Expr.True) { // if there's no case, don't add anything to the token
newCases.Add(Bpl.Expr.Binary(new NestedToken(cs.tok, kase.tok), Bpl.BinaryOperator.Opcode.And, cs, kase));
+ } else {
+ newCases.Add(cs);
}
}
}
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs index 68027609..1c7286e7 100644 --- a/Source/ModelViewer/Main.cs +++ b/Source/ModelViewer/Main.cs @@ -15,7 +15,6 @@ namespace Microsoft.Boogie.ModelViewer {
public partial class Main : Form
{
- string SearchText;
SkeletonItem unfoldingRoot;
SkeletonItem[] allItems;
int currentState, previousState = -1;
|