Use new, SMT2 compliant, Z3 syntax for labels

1 files changed, 3 insertions, 2 deletions

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index a2d6952c..7ac2e2bb 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -516,7 +516,8 @@ namespace Microsoft.Boogie.SMTLib
         var op = (VCExprLabelOp)node.Op;

         if (ExprLineariser.ProverOptions.UseLabels) {

           // Z3 extension

-          wr.Write("({0} {1} ", op.pos ? "lblpos" : "lblneg", SMTLibNamer.QuoteId(op.label));

+          //wr.Write("({0} {1} ", op.pos ? "lblpos" : "lblneg", SMTLibNamer.QuoteId(op.label));

+          wr.Write("(! ");

         }

 

         wr.Write("({0} {1} ", op.pos ? "and" : "or", SMTLibNamer.QuoteId(SMTLibNamer.LabelVar(op.label)));

@@ -526,7 +527,7 @@ namespace Microsoft.Boogie.SMTLib
         wr.Write(")");

 

         if (ExprLineariser.ProverOptions.UseLabels)

-          wr.Write(")");

+          wr.Write(" :{0} {1})", op.pos ? "lblpos" : "lblneg", SMTLibNamer.QuoteId(op.label));

 

         return true;

       }