From 3a281bac64e4a4ae27a277c78e505f4704ab20b0 Mon Sep 17 00:00:00 2001
From: kyessenov <unknown>
Date: Mon, 23 Aug 2010 20:25:11 +0000
Subject: Report a bug in Z3 instead of evil input "?"

---
 Source/Provers/Z3/Prover.cs | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'Source/Provers')

diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs
index 7a882888..c93b364d 100644
--- a/Source/Provers/Z3/Prover.cs
+++ b/Source/Provers/Z3/Prover.cs
@@ -271,6 +271,9 @@ namespace Microsoft.Boogie.Z3
           return ProverOutcome.TimeOut;
         }
 
+        if (ch == -1)
+            throw new UnexpectedProverOutputException("z3 crashed and produced no output");          
+        
         string line = new string((char)ch, 1) + FromReadLine();
 
         if (line.StartsWith("STATS ")) {
-- 
cgit v1.2.3