summaryrefslogtreecommitdiff
path: root/Source/Provers
diff options
context:
space:
mode:
authorGravatar MichalMoskal <unknown>2011-02-23 02:24:56 +0000
committerGravatar MichalMoskal <unknown>2011-02-23 02:24:56 +0000
commit80682670d13f84360d345576366190c3f054517f (patch)
tree2c540b29600a94f8f7c1cc6cae11a12aac7addfd /Source/Provers
parentd84f8e27637ab950a44ba493151e62912e366291 (diff)
Dispose of the prover when Close() is called.
Diffstat (limited to 'Source/Provers')
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs8
-rw-r--r--Source/Provers/SMTLib/SMTLibProcess.cs9
2 files changed, 17 insertions, 0 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 3b48bbbe..c8c10af9 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -203,6 +203,14 @@ namespace Microsoft.Boogie.SMTLib
}
}
+ public override void Close()
+ {
+ base.Close();
+ CloseLogFile();
+ if (Process != null)
+ Process.Close();
+ }
+
public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)
{
//Contract.Requires(descriptiveName != null);
diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index 7dbb1c59..a5fd1502 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -128,6 +128,15 @@ namespace Microsoft.Boogie.SMTLib
}
}
+ public void Close()
+ {
+ try {
+ prover.Kill();
+ } catch {
+ }
+ DisposeProver();
+ }
+
public event Action<string> ErrorHandler;
int errorCnt;