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)

---
 Test/aitest0/Answer | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'Test/aitest0/Answer')

diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer
index 18359b2e..dabe9710 100644
--- a/Test/aitest0/Answer
+++ b/Test/aitest0/Answer
@@ -119,5 +119,10 @@ Execution trace:
     Intervals.bpl(68,5): anon0
     Intervals.bpl(69,3): anon3_LoopHead
     Intervals.bpl(69,3): anon3_LoopDone
+Intervals.bpl(92,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    Intervals.bpl(87,5): anon0
+    Intervals.bpl(88,3): loop_head
+    Intervals.bpl(91,3): after_loop
 
-Boogie program verifier finished with 4 verified, 2 errors
+Boogie program verifier finished with 5 verified, 3 errors
-- 
cgit v1.2.3