From 3f4c65b26ce7771eeb1ef738eb65ef63be62a617 Mon Sep 17 00:00:00 2001
From: Unknown <akashl@MSRI-Akashlal.fareast.corp.microsoft.com>
Date: Sat, 25 Jun 2011 17:23:28 +0530
Subject: Avoid restarting the theorem prover for stratified inlining because
 it can lose context. Added a cache for FindLeastToVerify

---
 Source/BoogieDriver/BoogieDriver.cs | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'Source/BoogieDriver/BoogieDriver.cs')

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index dcc007fe..88d8bdaa 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -512,6 +512,12 @@ namespace Microsoft.Boogie {
                   }
                   outcome = svcgen.FindLeastToVerify(impl, program, ref ss);
                   errors = new List<Counterexample>();
+                  Console.Write("Result: ");
+                  foreach (var s in ss)
+                  {
+                      Console.Write("{0} ", s);
+                  }
+                  Console.WriteLine();
               }
               else
               {
-- 
cgit v1.2.3