Updates for the latest changes in Z3's SMT2 parser

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

           }

         }

       }