diff options
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/Check.cs | 25 | ||||
| -rw-r--r-- | Source/VCGeneration/Context.cs | 15 |
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>();
}
|