diff options
| author |  Rustan Leino <unknown> | 2013-07-05 14:37:39 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-07-05 14:37:39 -0700 |
| commit | ff756ddf4bb171ff6398199bfecf1d1f46a54225 (patch) | |
| tree | 5f915bbac861138ad6147e68cc8c7675d75fefe7 /Source/VCGeneration/Check.cs | |
| parent | 7fbe519af9271420e5b513021dd1f846a4337e7e (diff) | |
| parent | d54c349601e9a4da8d28919008c85ca990447ead (diff) | |
Merge
Diffstat (limited to 'Source/VCGeneration/Check.cs')
| -rw-r--r-- | Source/VCGeneration/Check.cs | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 3249708e..5fe0bcea 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -188,6 +188,7 @@ namespace Microsoft.Boogie { {
TheoremProver.SetTimeOut(0);
}
+ TheoremProver.Reset();
}
private static void Setup(Program prog, ProverContext ctx)
@@ -465,6 +466,10 @@ namespace Microsoft.Boogie { public virtual void Close() {
}
+ public void Reset()
+ {
+ }
+
/// <summary>
/// MSchaef: Allows to Push a VCExpression as Axiom on the prover stack (beta)
/// for now it is only implemented by ProcessTheoremProver and still requires some
|