diff options
author | wuestholz <unknown> | 2015-02-18 13:14:26 +0100 |
---|---|---|
committer | wuestholz <unknown> | 2015-02-18 13:14:26 +0100 |
commit | 2adff68a1579de5ba40c8b8713fc75a383e1ff91 (patch) | |
tree | 8dedaca6abe7c6cb98e2a983c569ea258514a755 /Source/VCExpr | |
parent | 59fdb656f09cb4f51fc60d30d8c1bef59f5f908d (diff) |
Added a setter for CommandLineOptions.ProverOptions and fixed several contracts.
Diffstat (limited to 'Source/VCExpr')
-rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 49dbb7c8..8674f8c0 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -316,7 +316,7 @@ namespace Microsoft.Boogie.VCExprAST { public override Expr VisitLiteralExpr(LiteralExpr node) {
//Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<LiteralExpr>() != null);
+ Contract.Ensures(Contract.Result<Expr>() != null);
Push(TranslateLiteralExpr(node));
return node;
}
@@ -456,14 +456,14 @@ namespace Microsoft.Boogie.VCExprAST { public override Expr VisitExistsExpr(ExistsExpr node) {
//Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<ExistsExpr>() != null);
+ Contract.Ensures(Contract.Result<Expr>() != null);
node = (ExistsExpr)this.VisitQuantifierExpr(node);
return node;
}
public override Expr VisitForallExpr(ForallExpr node) {
//Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<ForallExpr>() != null);
+ Contract.Ensures(Contract.Result<Expr>() != null);
node = (ForallExpr)this.VisitQuantifierExpr(node);
return node;
}
@@ -559,7 +559,7 @@ namespace Microsoft.Boogie.VCExprAST { public override Expr VisitBvExtractExpr(BvExtractExpr node) {
//Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<BvExtractExpr>() != null);
+ Contract.Ensures(Contract.Result<Expr>() != null);
Push(TranslateBvExtractExpr(node));
return node;
}
@@ -576,7 +576,7 @@ namespace Microsoft.Boogie.VCExprAST { public override Expr VisitBvConcatExpr(BvConcatExpr node) {
//Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<BvConcatExpr>() != null);
+ Contract.Ensures(Contract.Result<Expr>() != null);
Push(TranslateBvConcatExpr(node));
return node;
}
|