From a0331bcece67f35325fe70f2fda1b87d66397ab1 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Mon, 12 Dec 2011 13:52:36 -0800
Subject: Boogie: Changed Expr.Not to keep swap arguments rather change
 direction of operator when negating <, <=, >=, or >

---
 Test/inline/Answer | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'Test/inline')

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:
-- 
cgit v1.2.3