diff options
| author |  leino <unknown> | 2014-10-21 18:28:42 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-10-21 18:28:42 -0700 |
| commit | 13d181a688ef5a5f1acd72928f7bef12d146ebad (patch) | |
| tree | ba12e381748c1892e4e12e747fce7f65a6ad60d3 /Source/Dafny/Translator.cs | |
| parent | e94dc5817a729ebdd6786deb17e1903974c8b981 (diff) | |
When guessing decreases clauses for loops, convert numeric values to their ultimate base type (int or real) before subtracting
Diffstat (limited to 'Source/Dafny/Translator.cs')
| -rw-r--r-- | Source/Dafny/Translator.cs | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 1086a79b..4f0f3b61 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -7805,7 +7805,7 @@ namespace Microsoft.Dafny { }
} else if (F is BinaryExpr) {
var bin = (BinaryExpr)F;
- if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Add) {
+ if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Add && (bin.E0.Type.IsIntegerType || bin.E0.Type.IsRealType)) {
if (!ContainsFreeVariable(bin.E1, false, i)) {
// We're looking at: R(i) && j == f(i) + K.
// By a recursive call, we'll ask to invert: R(i) && j' == f(i).
@@ -7823,7 +7823,7 @@ namespace Microsoft.Dafny { yield return val.Subst(j, jMinusK, this);
}
}
- } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Sub) {
+ } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Sub && (bin.E0.Type.IsIntegerType || bin.E0.Type.IsRealType)) {
if (!ContainsFreeVariable(bin.E1, false, i)) {
// We're looking at: R(i) && j == f(i) - K
// Recurse on f(i) and then replace j := j + K
|