From efe732baac2d81573bdd220e41bffaedf1f9eab4 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Wed, 29 Jun 2011 16:50:57 -0700
Subject: Boogie: use (WEIGHT 0) with the select-of-store axioms

---
 Source/VCExpr/VCExprAST.cs | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'Source/VCExpr/VCExprAST.cs')

diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index bb0539bf..38541881 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -587,14 +587,18 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<VCExpr>() != null);
       return Quantify(Quantifier.ALL, typeParams, vars, triggers, infos, body);
     }
-    public VCExpr Forall(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, string qid, VCExpr body) {
+    public VCExpr Forall(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, string qid, int weight, VCExpr body) {
       Contract.Requires(body != null);
       Contract.Requires(qid != null);
       Contract.Requires(cce.NonNullElements(triggers));
       Contract.Requires(cce.NonNullElements(vars));
       Contract.Ensures(Contract.Result<VCExpr>() != null);
+      QKeyValue kv = null;
+      if (0 <= weight) {
+        kv = new QKeyValue(Token.NoToken, "weight", new List<object>() { new LiteralExpr(Token.NoToken, BigNum.FromInt(0)) }, null);
+      }
       return Quantify(Quantifier.ALL, new List<TypeVariable/*!*/>(), vars,
-                            triggers, new VCQuantifierInfos(qid, -1, false, null), body);
+                            triggers, new VCQuantifierInfos(qid, -1, false, kv), body);
     }
     public VCExpr Forall(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, VCExpr body) {
       Contract.Requires(body != null);
-- 
cgit v1.2.3