diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-06-29 16:50:57 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-06-29 16:50:57 -0700 |
| commit | efe732baac2d81573bdd220e41bffaedf1f9eab4 (patch) | |
| tree | 0edfc0fd97211a11006f2ddb7d23ec1ff80d200d /Source/VCExpr/VCExprAST.cs | |
| parent | 507b50ed1ccc51bbd24f3cea6f3c287b97b3d299 (diff) | |
Boogie: use (WEIGHT 0) with the select-of-store axioms
Diffstat (limited to 'Source/VCExpr/VCExprAST.cs')
| -rw-r--r-- | Source/VCExpr/VCExprAST.cs | 8 |
1 files changed, 6 insertions, 2 deletions
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);
|