From 19119542222cb54869e6bd691ed77667838743e2 Mon Sep 17 00:00:00 2001
From: Michal Moskal <michal@moskal.me>
Date: Thu, 28 Apr 2011 10:43:13 -0700
Subject: Use :reason-unknown not :last-failure for Z3 in SMT mode; disable
 SORT_AND_OR option (obsolete)

---
 Source/Provers/SMTLib/ProverInterface.cs | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'Source/Provers/SMTLib/ProverInterface.cs')

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index f1a00873..5efbb96f 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -435,10 +435,7 @@ namespace Microsoft.Boogie.SMTLib
       }
 
       if (wasUnknown) {
-        if (options.UseZ3)
-          SendThisVC("(get-info :last-failure)");
-        else
-          SendThisVC("(get-info :reason-unknown)");
+        SendThisVC("(get-info :reason-unknown)");
         Process.Ping();
 
         while (true) {
@@ -446,7 +443,7 @@ namespace Microsoft.Boogie.SMTLib
           if (resp == null || Process.IsPong(resp))
             break;
 
-          if (resp.ArgCount == 1 && (resp.Name == ":reason-unknown" || resp.Name == ":last-failure")) {
+          if (resp.ArgCount == 1 && resp.Name == ":reason-unknown") {
             switch (resp[0].Name) {
               case "memout":
                 result = Outcome.OutOfMemory;
-- 
cgit v1.2.3


From 0d9a18e7b1c75b184a2de1164db5fd4d41377c30 Mon Sep 17 00:00:00 2001
From: Michal Moskal <michal@moskal.me>
Date: Thu, 28 Apr 2011 10:51:50 -0700
Subject: Fix parsing of (labels) Z3 response; complain about unrecognized
 responses there

---
 Source/Provers/SMTLib/ProverInterface.cs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'Source/Provers/SMTLib/ProverInterface.cs')

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 5efbb96f..11b6e2db 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -371,7 +371,7 @@ namespace Microsoft.Boogie.SMTLib
         if (resp == null || Process.IsPong(resp))
           break;
         if (resp.Name == "labels" && resp.ArgCount >= 1) {
-          var labels = resp[0].Arguments.Select(a => a.Name.Replace("|", "")).ToArray();
+          var labels = resp.Arguments.Select(a => a.Name.Replace("|", "")).ToArray();
           res = labels;
           if (labelNums != null) HandleProverError("Got multiple :labels responses");
           labelNums = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList();
@@ -392,6 +392,8 @@ namespace Microsoft.Boogie.SMTLib
               theModel = models[0];
             }
           }
+        } else {
+          HandleProverError("Unexpected prover response (getting labels/model): " + resp.ToString());
         }
       }
 
-- 
cgit v1.2.3