From 277530c4a3dbdc7f82ba9ce4f628f30172110f91 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Mon, 8 Jul 2013 15:33:39 -0700
Subject: Worked on the parallelization.

---
 Source/VCGeneration/Check.cs   | 25 ++++++++++++++++---------
 Source/VCGeneration/Context.cs | 15 +++++++++++----
 2 files changed, 27 insertions(+), 13 deletions(-)

(limited to 'Source/VCGeneration')

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index a3f266ef..1e588760 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -178,17 +178,23 @@ namespace Microsoft.Boogie {
 
     public void Retarget(Program prog, ProverContext ctx, int timeout = 0)
     {
+        TheoremProver.FullReset();
         ctx.Clear();
         Setup(prog, ctx);
-        if (0 < timeout)
-        {
-          TheoremProver.SetTimeOut(timeout * 1000);
-        }
-        else
-        {
-          TheoremProver.SetTimeOut(0);
-        }
-        TheoremProver.FullReset();
+        this.timeout = timeout;
+        SetTimeout();
+    }
+
+    public void SetTimeout()
+    {
+      if (0 < timeout)
+      {
+        TheoremProver.SetTimeOut(timeout * 1000);
+      }
+      else
+      {
+        TheoremProver.SetTimeOut(0);
+      }
     }
 
     private static void Setup(Program prog, ProverContext ctx)
@@ -316,6 +322,7 @@ namespace Microsoft.Boogie {
       this.handler = handler;
 
       thmProver.Reset();
+      SetTimeout();
       proverStart = DateTime.UtcNow;
       thmProver.BeginCheck(descriptiveName, vc, handler);
       //  gen.ClearSharedFormulas();    PR: don't know yet what to do with this guy
diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs
index 484ce226..a836b6fb 100644
--- a/Source/VCGeneration/Context.cs
+++ b/Source/VCGeneration/Context.cs
@@ -104,10 +104,8 @@ public abstract class ProverContextContracts:ProverContext{
       this.genOptions = genOptions;
       Boogie2VCExprTranslator t = new Boogie2VCExprTranslator (gen, genOptions);
       this.translator = t;
-      OrderingAxiomBuilder oab = new OrderingAxiomBuilder(gen, t);
-      Contract.Assert(oab != null);
-      oab.Setup();
-      this.orderingAxiomBuilder = oab;
+
+      SetupOrderingAxiomBuilder(gen, t);
 
       distincts = new List<Variable>();
       axiomConjuncts = new List<VCExpr>();
@@ -115,8 +113,17 @@ public abstract class ProverContextContracts:ProverContext{
       exprTranslator = null;
     }
 
+    private void SetupOrderingAxiomBuilder(VCExpressionGenerator gen, Boogie2VCExprTranslator t)
+    {
+      OrderingAxiomBuilder oab = new OrderingAxiomBuilder(gen, t);
+      Contract.Assert(oab != null);
+      oab.Setup();
+      this.orderingAxiomBuilder = oab;
+    }
+
     public override void Clear()
     {
+        SetupOrderingAxiomBuilder(gen, translator);
         distincts = new List<Variable>();
         axiomConjuncts = new List<VCExpr>();
     }
-- 
cgit v1.2.3