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/Provers/Simplify/ProverInterface.cs | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'Source/Provers/Simplify')

diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs
index 68c02c5d..95d8950a 100644
--- a/Source/Provers/Simplify/ProverInterface.cs
+++ b/Source/Provers/Simplify/ProverInterface.cs
@@ -511,7 +511,13 @@ namespace Microsoft.Boogie.Simplify {
           thmProver = null;
           currentProverHasBeenABadBoy = false;
           restarts++;
+
+          if (CommandLineOptions.Clo.StratifiedInlining > 0)
+          {
+              Console.WriteLine("Warning: restarting theorem prover. Context could be lost");
+          }
         }
+          
         FireUpNewProver();
       }
       cce.EndExpose();
-- 
cgit v1.2.3