From 1ea222005d9d4722457f70cbd771fde5eed4d76f Mon Sep 17 00:00:00 2001
From: schaef <unknown>
Date: Fri, 20 Nov 2009 09:24:55 +0000
Subject:

---
 Source/VCGeneration/DoomCheck.ssc | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'Source')

diff --git a/Source/VCGeneration/DoomCheck.ssc b/Source/VCGeneration/DoomCheck.ssc
index cdbdcb6a..ecefedea 100644
--- a/Source/VCGeneration/DoomCheck.ssc
+++ b/Source/VCGeneration/DoomCheck.ssc
@@ -313,7 +313,7 @@ namespace VC
                         
                             ConsoleColor col = Console.ForegroundColor;
                             Console.ForegroundColor = ConsoleColor.Blue; 
-                            Console.WriteLine("Assert false was detected, but ignored");
+                            Console.WriteLine("Assert false or PossiblyUnreachable was detected, but ignored");
                             Console.ForegroundColor = col;                                              
 
                             currentNode.HasBeenChecked = true;  
@@ -365,12 +365,12 @@ namespace VC
                 }
                 return false;
             }
-            
+
             private bool BlockContainsAssertFalse(Block! b) {
                 foreach (Cmd! c in b.Cmds) {
                     AssertCmd ac = c as AssertCmd;
                     if (ac!=null) {
-                        if (IsFalse(ac.Expr) ) {
+                        if (IsFalse(ac.Expr) || QKeyValue.FindBoolAttribute(ac.Attributes, "PossiblyUnreachable") ) {
                             return true;
                         }
                     }
-- 
cgit v1.2.3