From 2adff68a1579de5ba40c8b8713fc75a383e1ff91 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Wed, 18 Feb 2015 13:14:26 +0100
Subject: Added a setter for CommandLineOptions.ProverOptions and fixed several
 contracts.

---
 Source/VCExpr/Boogie2VCExpr.cs | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'Source/VCExpr')

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;
     }
-- 
cgit v1.2.3