commented calls to GC.Collect()

2 files changed, 10 insertions, 6 deletions

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index 3cb27e14..b0c8fabf 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -18,6 +18,7 @@ using VC;
 

 namespace Microsoft.Boogie.Houdini {

   public class HoudiniSession {

+    public static double proverTime = 0;

     private string descriptiveName;

     private VCExpr conjecture;

     private ProverInterface.ErrorHandler handler;

@@ -49,10 +50,13 @@ namespace Microsoft.Boogie.Houdini {
     public ProverInterface.Outcome Verify(Checker checker, VCExpr axiom, out List<Counterexample> errors) {

       collector.examples.Clear();

       VCExpr vc = checker.VCExprGen.Implies(axiom, conjecture);

+

+      DateTime now = DateTime.Now;

       checker.BeginCheck(descriptiveName, vc, handler);

       WaitHandle.WaitAny(new WaitHandle[] { checker.ProverDone });

-

       ProverInterface.Outcome proverOutcome = checker.ReadOutcome();

+      proverTime += (DateTime.Now - now).TotalSeconds;

+

       if (proverOutcome == ProverInterface.Outcome.Invalid) {

         Contract.Assume(collector.examples != null);

         if (collector.examples.Count == 0) {

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 06fd5502..27b8d05f 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -686,7 +686,7 @@ namespace Microsoft.Boogie.Houdini {
       this.NotifyStart(program, houdiniConstants.Keys.Count);

 

       while (current.WorkList.Count > 0) {

-        System.GC.Collect();

+        //System.GC.Collect();

         this.NotifyIteration();

 

         VCExpr axiom = BuildAxiom(current.Assignment);

@@ -722,7 +722,7 @@ namespace Microsoft.Boogie.Houdini {
 

       while (current.WorkList.Count > 0) {

         bool exceptional = false;

-        System.GC.Collect();

+        //System.GC.Collect();

         this.NotifyIteration();

 

         current.Implementation = current.WorkList.Peek();

@@ -763,7 +763,7 @@ namespace Microsoft.Boogie.Houdini {
 

       while (current.WorkList.Count > 0) {

         bool exceptional = false;

-        System.GC.Collect();

+        //System.GC.Collect();

         this.NotifyIteration();

 

         current.Implementation = current.WorkList.Peek();

@@ -960,7 +960,7 @@ namespace Microsoft.Boogie.Houdini {
 

         do {

           if (pastFirstIter) {

-            System.GC.Collect();

+            //System.GC.Collect();

             this.NotifyIteration();

           }

 

@@ -1027,7 +1027,7 @@ namespace Microsoft.Boogie.Houdini {
           outcome = ProverInterface.Outcome.Undetermined;

 

           if (pastFirstIter) {

-            System.GC.Collect();

+            //System.GC.Collect();

             this.NotifyIteration();

           }