diff options
Diffstat (limited to 'Source')
-rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 8 | ||||
-rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 6 |
2 files changed, 7 insertions, 7 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 6e59477b..f1a00873 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -357,9 +357,9 @@ namespace Microsoft.Boogie.SMTLib private string[] GetLabelsInfo(ErrorHandler handler)
{
- SendThisVC("(get-info :labels)");
+ SendThisVC("(labels)");
if (options.ExpectingModel())
- SendThisVC("(get-info :model)");
+ SendThisVC("(model)");
Process.Ping();
List<string> labelNums = null;
@@ -370,12 +370,12 @@ namespace Microsoft.Boogie.SMTLib var resp = Process.GetProverResponse();
if (resp == null || Process.IsPong(resp))
break;
- if (resp.Name == ":labels" && resp.ArgCount >= 1) {
+ if (resp.Name == "labels" && resp.ArgCount >= 1) {
var labels = resp[0].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();
- } else if (resp.Name == ":model" && resp.ArgCount >= 1) {
+ } else if (resp.Name == "model" && resp.ArgCount >= 1) {
var modelStr = resp[0].Name;
List<Model> models = null;
try {
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 7ac2e2bb..d06cba3b 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -262,7 +262,7 @@ namespace Microsoft.Boogie.SMTLib if (hasAttrs) {
wr.Write("\n");
if (infos.qid != null)
- wr.Write(" :named {0}\n", SMTLibNamer.QuoteId(infos.qid));
+ wr.Write(" :qid {0}\n", SMTLibNamer.QuoteId(infos.qid));
if (weight != 1)
wr.Write(" :weight {0}\n", weight);
if (infos.uniqueId != -1)
@@ -326,10 +326,10 @@ namespace Microsoft.Boogie.SMTLib foreach (VCTrigger vcTrig in triggers) {
Contract.Assert(vcTrig != null);
if (!vcTrig.Pos) {
- wr.Write(" :no-pattern (");
+ wr.Write(" :no-pattern ");
Contract.Assert(vcTrig.Exprs.Count == 1);
Linearise(vcTrig.Exprs[0], options);
- wr.Write(")\n");
+ wr.Write("\n");
}
}
}
|