Support {:PossiblyUnreachable} attribute on asserts

1 files changed, 7 insertions, 1 deletions

diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc
index 6e5b147b..7a3a772c 100644
--- a/Source/VCGeneration/VC.ssc
+++ b/Source/VCGeneration/VC.ssc
@@ -242,7 +242,13 @@ namespace VC
 

       bool CheckUnreachable(Block! cur, CmdSeq! seq)

         throws UnexpectedProverOutputException;

-       {

+      {

+        foreach (Cmd cmd in seq) {

+          AssertCmd assrt = cmd as AssertCmd;

+          if (assrt != null && QKeyValue.FindBoolAttribute(assrt.Attributes, "PossiblyUnreachable"))

+            return false;

+        }

+

         DateTime start = DateTime.Now;

         if (CommandLineOptions.Clo.Trace) {

           System.Console.Write("    soundness smoke test #{0} ... ", id);