diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-12-12 13:52:36 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-12-12 13:52:36 -0800 |
| commit | a0331bcece67f35325fe70f2fda1b87d66397ab1 (patch) | |
| tree | 29a3325b513466bbd112c50d7ccd101277ef3773 | |
| parent | b476991da92ea85c4d1a3cad84dc5171e08a4cf8 (diff) | |
Boogie: Changed Expr.Not to keep swap arguments rather change direction of operator when negating <, <=, >=, or >
| -rw-r--r-- | Source/Core/AbsyExpr.cs | 8 | ||||
| -rw-r--r-- | Test/inline/Answer | 6 |
2 files changed, 7 insertions, 7 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 02a2f762..e274fcc3 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -197,13 +197,13 @@ namespace Microsoft.Boogie { } else if (op.Op == BinaryOperator.Opcode.Neq) {
return Eq(arg0, arg1);
} else if (op.Op == BinaryOperator.Opcode.Lt) {
- return Ge(arg0, arg1);
+ return Le(arg1, arg0);
} else if (op.Op == BinaryOperator.Opcode.Le) {
- return Gt(arg0, arg1);
+ return Lt(arg1, arg0);
} else if (op.Op == BinaryOperator.Opcode.Ge) {
- return Lt(arg0, arg1);
+ return Gt(arg1, arg0);
} else if (op.Op == BinaryOperator.Opcode.Gt) {
- return Le(arg0, arg1);
+ return Ge(arg1, arg0);
}
}
}
diff --git a/Test/inline/Answer b/Test/inline/Answer index 6f63f1e3..eb409cc2 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -591,7 +591,7 @@ implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: in goto anon4_LoopHead;
anon4_LoopDone:
- assume i >= size;
+ assume size <= i;
goto anon3;
anon3:
@@ -714,7 +714,7 @@ implementation main(x: int) goto inline$find$0$anon4_LoopHead;
inline$find$0$anon4_LoopDone:
- assume inline$find$0$i >= inline$find$0$size;
+ assume inline$find$0$size <= inline$find$0$i;
goto inline$find$0$anon3;
inline$find$0$anon3:
@@ -811,7 +811,7 @@ implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: in goto anon4_LoopHead;
anon4_LoopDone:
- assume i >= size;
+ assume size <= i;
goto anon3;
anon3:
|