From 32fe52ad799e68b6d1531b1cef81910b7b20424d Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Sat, 2 Apr 2011 01:05:31 +0000
Subject: Use new, SMT2 compliant, Z3 syntax for labels

---
 Source/Provers/SMTLib/SMTLibLineariser.cs | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')

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;
       }
-- 
cgit v1.2.3