From 52e2ae918c077e39858f8264d76bd267e60c7f34 Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Wed, 23 Feb 2011 00:48:50 +0000
Subject: Pass :skolemid to SMTLib prover

---
 Source/Provers/SMTLib/SMTLibLineariser.cs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'Source/Provers')

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 3c6c611c..4cec5ad4 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -245,7 +245,7 @@ namespace Microsoft.Boogie.SMTLib
         var weight = QKeyValue.FindIntAttribute(infos.attributes, "weight", 1);
         if (!ProverOptions.UseWeights)
           weight = 1;
-        var hasAttrs = node.Triggers.Count > 0 || infos.qid != null || weight != 1;
+        var hasAttrs = node.Triggers.Count > 0 || infos.qid != null || weight != 1 || infos.uniqueId != -1;
 
         if (hasAttrs)
           wr.Write("(! ");
@@ -258,6 +258,8 @@ namespace Microsoft.Boogie.SMTLib
             wr.Write(" :named {0}\n", SMTLibNamer.QuoteId(infos.qid));
           if (weight != 1)
             wr.Write(" :weight {0}\n", weight);
+          if (infos.uniqueId != -1)
+            wr.Write(" :skolemid {0}\n", infos.uniqueId);
           WriteTriggers(node.Triggers, options);
           
           wr.Write(")");
-- 
cgit v1.2.3