diff options
author | 2011-04-28 10:51:50 -0700 | |
---|---|---|
committer | 2011-04-28 10:51:50 -0700 | |
commit | 0d9a18e7b1c75b184a2de1164db5fd4d41377c30 (patch) | |
tree | 2dfec6724acb18a7730b2f0828a6a6b1a135177e /Source/Provers/SMTLib/ProverInterface.cs | |
parent | 19119542222cb54869e6bd691ed77667838743e2 (diff) |
Fix parsing of (labels) Z3 response; complain about unrecognized responses there
Diffstat (limited to 'Source/Provers/SMTLib/ProverInterface.cs')
-rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 4 |
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());
}
}
|