diff options
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibProcess.cs')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibProcess.cs | 27 |
1 files changed, 18 insertions, 9 deletions
diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs index 8cc67256..b23fddbb 100644 --- a/Source/Provers/SMTLib/SMTLibProcess.cs +++ b/Source/Provers/SMTLib/SMTLibProcess.cs @@ -71,7 +71,7 @@ namespace Microsoft.Boogie.SMTLib public bool IsPong(SExpr sx)
{
- return sx.Name == ":name";
+ return sx != null && sx.Name == ":name";
}
public void PingPong()
@@ -79,6 +79,11 @@ namespace Microsoft.Boogie.SMTLib Ping();
while (true) {
var sx = GetProverResponse();
+ if (sx == null) {
+ ErrorHandler("Prover died");
+ return;
+ }
+
if (IsPong(sx))
return;
else
@@ -261,21 +266,25 @@ namespace Microsoft.Boogie.SMTLib void prover_OutputDataReceived(object sender, DataReceivedEventArgs e)
{
lock (this) {
- if (options.Verbosity >= 2 || (options.Verbosity >= 1 && !e.Data.StartsWith("(:name"))) {
- Console.WriteLine("[SMT-OUT] {0}", e.Data);
+ if (e.Data != null) {
+ if (options.Verbosity >= 2 || (options.Verbosity >= 1 && !e.Data.StartsWith("(:name "))) {
+ Console.WriteLine("[SMT-OUT] {0}", e.Data);
+ }
+ proverOutput.Enqueue(e.Data);
+ Monitor.Pulse(this);
}
- proverOutput.Enqueue(e.Data);
- Monitor.Pulse(this);
}
}
void prover_ErrorDataReceived(object sender, DataReceivedEventArgs e)
{
lock (this) {
- if (options.Verbosity >= 1)
- Console.WriteLine("[SMT-ERR] {0}", e.Data);
- proverErrors.Enqueue(e.Data);
- Monitor.Pulse(this);
+ if (e.Data != null) {
+ if (options.Verbosity >= 1)
+ Console.WriteLine("[SMT-ERR] {0}", e.Data);
+ proverErrors.Enqueue(e.Data);
+ Monitor.Pulse(this);
+ }
}
}
#endregion
|