From 08e9539279d31cfb650e0e55984216f5c8ffcd25 Mon Sep 17 00:00:00 2001
From: qadeer <qadeer@microsoft.com>
Date: Thu, 29 Dec 2011 14:43:03 -0800
Subject: fixed problems with datatypes removed stale contracts in stratified
 inlining added test to datatypes

---
 Source/VCGeneration/ConditionGeneration.cs | 2 --
 1 file changed, 2 deletions(-)

(limited to 'Source/VCGeneration/ConditionGeneration.cs')

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 26361cdf..ed698d5f 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -25,12 +25,10 @@ namespace Microsoft.Boogie {
 
     [ContractInvariantMethod]
     void ObjectInvariant() {
-      Contract.Invariant(counterexample != null);
       Contract.Invariant(cce.NonNullElements(args));
     }
 
     public CalleeCounterexampleInfo(Counterexample cex, List<Model.Element/*!>!*/> x) {
-      Contract.Requires(cex != null);
       Contract.Requires(cce.NonNullElements(x));
       counterexample = cex;
       args = x;
-- 
cgit v1.2.3