diff options
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);
|