Fix parsing of (labels) Z3 response; complain about unrecognized responses there

1 files changed, 3 insertions, 1 deletions

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());

         }

       }