From ecd49b32f40d6a0683beb89a8ae7cc2ba40d853f Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Thu, 30 May 2013 14:17:40 -0700
Subject: Fixed bug in Interval abstract domain (pertaining to unary negation)

---
 Source/AbsInt/IntervalDomain.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Source/AbsInt')

diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index 3d83bb5c..be62eb58 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -667,7 +667,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
               Lo = 1 - hi;
             }
             if (lo != null) {
-              Hi = -lo;
+              Hi = 1 - lo;
             }
           }
           else if (op.Op == UnaryOperator.Opcode.Not) {
-- 
cgit v1.2.3