Worked on the parallelization.

2 files changed, 27 insertions, 13 deletions

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>();

     }