diff options
author | wuestholz <unknown> | 2013-07-08 15:33:39 -0700 |
---|---|---|
committer | wuestholz <unknown> | 2013-07-08 15:33:39 -0700 |
commit | 277530c4a3dbdc7f82ba9ce4f628f30172110f91 (patch) | |
tree | 419b65222890b799ac5e05b8f635b72e9a0c14c9 /Source/VCGeneration/Check.cs | |
parent | 11e2d2b6d6a8cb6da6d98bc8f102d8375fca26f5 (diff) |
Worked on the parallelization.
Diffstat (limited to 'Source/VCGeneration/Check.cs')
-rw-r--r-- | Source/VCGeneration/Check.cs | 25 |
1 files changed, 16 insertions, 9 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
|